[STATEMENT]
theorem (in Congruence_Rule) Ang_complementary :
  assumes
    "Def (Ang (An A B C))"
    "Def (Ang (An A1 B1 C1))"
    "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)"
    "Bet_Point (Se A D) B"
    "Bet_Point (Se A1 D1) B1"
  shows
    "Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp)
    \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp)
    \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
[PROOF STEP]
by (simp add:Ang_replace)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))
[PROOF STEP]
obtain A2 :: Point where P1 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp)
    \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2
    \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 A1) p \<and> \<not> Bet_Point (Se p A1) B1 \<and> Def (Ang (An p B1 C1))

goal (1 subgoal):
 1. (\<And>A2. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp)
    \<and> Eq (Geos (Ang (An A2 B1 C1)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp)
    \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp)
    \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A2 B1 p))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A2 B1 C1)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A2 B1 p))
[PROOF STEP]
by (simp add:Ang_replace)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A2 B1 C1)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A2 B1 p))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A2 B1 C1)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A2 B1 p))
[PROOF STEP]
obtain C2 :: Point where P2 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp)
    \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2
    \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Ang (An A2 B1 C1)) add Emp) (Geos (Ang (An A2 B1 p)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Line_on (Li B1 C1) p \<and> \<not> Bet_Point (Se p C1) B1 \<and> Def (Ang (An A2 B1 p))

goal (1 subgoal):
 1. (\<And>C2. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Def (Tri (Tr A B C))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A B C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P3 : "Def (Tri (Tr B A C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

goal (1 subgoal):
 1. Def (Tri (Tr B A C))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B A C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))
[PROOF STEP]
have "Def (Tri (Tr A2 B1 C2))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))

goal (1 subgoal):
 1. Def (Tri (Tr A2 B1 C2))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A2 B1 C2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A2 B1 C2))
[PROOF STEP]
have P4 : "Def (Tri (Tr B1 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A2 B1 C2))

goal (1 subgoal):
 1. Def (Tri (Tr B1 A2 C2))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B1 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P1 P2 P3 P4
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))
Def (Tri (Tr B A C))
Def (Tri (Tr B1 A2 C2))
[PROOF STEP]
have P5 : "Cong (Geos (Tri (Tr B A C)) add Emp) (Geos (Tri (Tr B1 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))
Def (Tri (Tr B A C))
Def (Tri (Tr B1 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr B A C)) add Emp) (Geos (Tri (Tr B1 A2 C2)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr B A C)) add Emp) (Geos (Tri (Tr B1 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr B A C)) add Emp) (Geos (Tri (Tr B1 A2 C2)) add Emp)
[PROOF STEP]
have P6 : "Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr B A C)) add Emp) (Geos (Tri (Tr B1 A2 C2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr B A C)) add Emp) (Geos (Tri (Tr B1 A2 C2)) add Emp)
[PROOF STEP]
have P7 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr B A C)) add Emp) (Geos (Tri (Tr B1 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P8 : "Line_on (Li B1 D1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 D1) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 D1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P9 : "Line_on (Li A1 D1) B1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Line_on (Li A1 D1) B1
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 D1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have p10 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P11 : "Line_on (Li B1 A1) D1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Line_on (Li B1 A1) D1
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 A1) D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P12 : "Line_on (Li B1 D1) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 D1) D1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 D1) D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P13 : "Line_on (Li B1 A1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 A1) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 A1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P14 : "\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P8 P11 P12 P13 P14
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 D1) B1
Line_on (Li B1 A1) D1
Line_on (Li B1 D1) D1
Line_on (Li B1 A1) B1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
have P15 : "Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 D1) B1
Line_on (Li B1 A1) D1
Line_on (Li B1 D1) D1
Line_on (Li B1 A1) B1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 D1)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P1 P15
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 D1)) add Emp)
[PROOF STEP]
have P16 : "Line_on (Li B1 D1) A2"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 D1)) add Emp)

goal (1 subgoal):
 1. Line_on (Li B1 D1) A2
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 D1) A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B1 A2 C2))
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B1 A2 C2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P18 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P19 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P8 P16 P17 P19
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 D1) B1
Line_on (Li B1 D1) A2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 p)) add Emp)
    \<and> Bet_Point (Se p A2) B1 \<and> Line_on (Li B1 D1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 D1) B1
Line_on (Li B1 D1) A2
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Bet_Point (Se p A2) B1 \<and> Line_on (Li B1 D1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by (simp add:Seg_move_diffside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Bet_Point (Se p A2) B1 \<and> Line_on (Li B1 D1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Bet_Point (Se p A2) B1 \<and> Line_on (Li B1 D1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain D2 :: Point where P20 : "Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp)
    \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 p)) add Emp) \<and> Bet_Point (Se p A2) B1 \<and> Line_on (Li B1 D1) p \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>D2. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
[PROOF STEP]
have P21 : "Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A2 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A2 B1)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A2 B1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have P22 : "Bet_Point (Se A2 D2) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se A2 D2) B1
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A2 D2) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms P20 P21 P22
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A2 B1)) add Emp)
Bet_Point (Se A2 D2) B1
[PROOF STEP]
have P23 : "Eq (Geos (Seg (Se A D)) add Emp) (Geos (Seg (Se A2 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A2 B1)) add Emp)
Bet_Point (Se A2 D2) B1

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A D)) add Emp) (Geos (Seg (Se A2 D2)) add Emp)
[PROOF STEP]
by (blast intro:Seg_Bet_add)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A D)) add Emp) (Geos (Seg (Se A2 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B A C))
[PROOF STEP]
have P24 : "Def (Tri (Tr C A B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B A C))

goal (1 subgoal):
 1. Def (Tri (Tr C A B))
[PROOF STEP]
by (blast intro:Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C A B))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P25 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P26 : "Line_on (Li A B) D"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Line_on (Li A B) D
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) D

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P24 P25 P26
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C A B))
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Line_on (Li A B) D
[PROOF STEP]
have P27 : "Def (Tri (Tr C A D))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C A B))
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Line_on (Li A B) D

goal (1 subgoal):
 1. Def (Tri (Tr C A D))
[PROOF STEP]
by (simp add:Tri_def_extension)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C A D))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B1 A2 C2))
[PROOF STEP]
have P28 : "Def (Tri (Tr C2 A2 B1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B1 A2 C2))

goal (1 subgoal):
 1. Def (Tri (Tr C2 A2 B1))
[PROOF STEP]
by (blast intro:Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C2 A2 B1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P22
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A2 D2) B1
[PROOF STEP]
have P29 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi D2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A2 D2) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P22
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A2 D2) B1
[PROOF STEP]
have P30 : "Line_on (Li A2 B1) D2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A2 D2) B1

goal (1 subgoal):
 1. Line_on (Li A2 B1) D2
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B1) D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P28 P29 P30
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 A2 B1))
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi D2) add Emp)
Line_on (Li A2 B1) D2
[PROOF STEP]
have P31 : "Def (Tri (Tr C2 A2 D2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 A2 B1))
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi D2) add Emp)
Line_on (Li A2 B1) D2

goal (1 subgoal):
 1. Def (Tri (Tr C2 A2 D2))
[PROOF STEP]
by (simp add:Tri_def_extension)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C2 A2 D2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P24
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C A B))
[PROOF STEP]
have P32 : "Def (Ang (An C A B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C A B))

goal (1 subgoal):
 1. Def (Ang (An C A B))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C A B))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P27
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C A D))
[PROOF STEP]
have P33 : "Def (Ang (An C A D))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C A D))

goal (1 subgoal):
 1. Def (Ang (An C A D))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C A D))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P34 : "Line_on (Li A C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) C

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P35 : "\<not> Bet_Point (Se C C) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C C) A
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C C) A

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have "Inv (Bet_Point (Se D B) A)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Inv (Bet_Point (Se D B) A)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se D B) A)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se D B) A)
[PROOF STEP]
have "\<not> Bet_Point (Se D B) A"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se D B) A)

goal (1 subgoal):
 1. \<not> Bet_Point (Se D B) A
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se D B) A

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se D B) A
[PROOF STEP]
have P36 : "\<not> Bet_Point (Se B D) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se D B) A

goal (1 subgoal):
 1. \<not> Bet_Point (Se B D) A
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B D) A

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P33
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A D))
[PROOF STEP]
have "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A D))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P37 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P25 P26 P32 P33 P34 P35 P36 P37
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Line_on (Li A B) D
Def (Ang (An C A B))
Def (Ang (An C A D))
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
\<not> Bet_Point (Se B D) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P38 : "Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)
Line_on (Li A B) D
Def (Ang (An C A B))
Def (Ang (An C A D))
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
\<not> Bet_Point (Se B D) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A D)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P28
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 A2 B1))
[PROOF STEP]
have P39 : "Def (Ang (An C2 A2 B1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 A2 B1))

goal (1 subgoal):
 1. Def (Ang (An C2 A2 B1))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C2 A2 B1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P31
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 A2 D2))
[PROOF STEP]
have P40 : "Def (Ang (An C2 A2 D2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 A2 D2))

goal (1 subgoal):
 1. Def (Ang (An C2 A2 D2))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C2 A2 D2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P41 : "Line_on (Li A2 C2) C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 C2) C2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 C2) C2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P42 : "\<not> Bet_Point (Se C2 C2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C2 C2) A2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C2 C2) A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have "Inv (Bet_Point (Se B1 D2) A2)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Inv (Bet_Point (Se B1 D2) A2)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se B1 D2) A2)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se B1 D2) A2)
[PROOF STEP]
have P43 : "\<not> Bet_Point (Se B1 D2) A2"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se B1 D2) A2)

goal (1 subgoal):
 1. \<not> Bet_Point (Se B1 D2) A2
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B1 D2) A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C2 A2 D2))
[PROOF STEP]
have "\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C2 A2 D2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P44 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P29 P30 P39 P40 P41 P42 P43 P44
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi D2) add Emp)
Line_on (Li A2 B1) D2
Def (Ang (An C2 A2 B1))
Def (Ang (An C2 A2 D2))
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2
\<not> Bet_Point (Se B1 D2) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P45 : "Eq (Geos (Ang (An C2 A2 B1)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi D2) add Emp)
Line_on (Li A2 B1) D2
Def (Ang (An C2 A2 B1))
Def (Ang (An C2 A2 D2))
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2
\<not> Bet_Point (Se B1 D2) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An C2 A2 B1)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C2 A2 B1)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P7 P38
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A D)) add Emp)
[PROOF STEP]
have P46 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A D)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P45 P46
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An C2 A2 B1)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)
[PROOF STEP]
have P47 : "Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An C2 A2 B1)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 B1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Eq_rev Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P27
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C A D))
[PROOF STEP]
have P48 : "Def (Tri (Tr A C D))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C A D))

goal (1 subgoal):
 1. Def (Tri (Tr A C D))
[PROOF STEP]
by (blast intro:Tri_def_trans Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A C D))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P31
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 A2 D2))
[PROOF STEP]
have P49 : "Def (Tri (Tr A2 C2 D2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 A2 D2))

goal (1 subgoal):
 1. Def (Tri (Tr A2 C2 D2))
[PROOF STEP]
by (blast intro:Tri_def_trans Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A2 C2 D2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P6 P23 P47 P48 P49
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
Eq (Geos (Seg (Se A D)) add Emp) (Geos (Seg (Se A2 D2)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)
Def (Tri (Tr A C D))
Def (Tri (Tr A2 C2 D2))
[PROOF STEP]
have P50 : "Cong (Geos (Tri (Tr A C D)) add Emp) (Geos (Tri (Tr A2 C2 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
Eq (Geos (Seg (Se A D)) add Emp) (Geos (Seg (Se A2 D2)) add Emp)
Cong (Geos (Ang (An C A D)) add Emp) (Geos (Ang (An C2 A2 D2)) add Emp)
Def (Tri (Tr A C D))
Def (Tri (Tr A2 C2 D2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A C D)) add Emp) (Geos (Tri (Tr A2 C2 D2)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr A C D)) add Emp) (Geos (Tri (Tr A2 C2 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr A C D)) add Emp) (Geos (Tri (Tr A2 C2 D2)) add Emp)
[PROOF STEP]
have P51 : "Cong (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr A C D)) add Emp) (Geos (Tri (Tr A2 C2 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P50
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr A C D)) add Emp) (Geos (Tri (Tr A2 C2 D2)) add Emp)
[PROOF STEP]
have "Eq (Geos (Seg (Se C D)) add Emp) (Geos (Seg (Se C2 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr A C D)) add Emp) (Geos (Tri (Tr A2 C2 D2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se C D)) add Emp) (Geos (Seg (Se C2 D2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C D)) add Emp) (Geos (Seg (Se C2 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se C D)) add Emp) (Geos (Seg (Se C2 D2)) add Emp)
[PROOF STEP]
have P52 : "Eq (Geos (Seg (Se D C)) add Emp) (Geos (Seg (Se D2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se C D)) add Emp) (Geos (Seg (Se C2 D2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se D C)) add Emp) (Geos (Seg (Se D2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se D C)) add Emp) (Geos (Seg (Se D2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P53 : "Line_on (Li D A) B"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Line_on (Li D A) B
[PROOF STEP]
by (simp add:Bet_rev Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li D A) B

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have "Inv (Bet_Point (Se B A) D)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Inv (Bet_Point (Se B A) D)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se B A) D)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se B A) D)
[PROOF STEP]
have "\<not> Bet_Point (Se B A) D"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se B A) D)

goal (1 subgoal):
 1. \<not> Bet_Point (Se B A) D
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B A) D

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se B A) D
[PROOF STEP]
have P54 : "\<not> Bet_Point (Se A B) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se B A) D

goal (1 subgoal):
 1. \<not> Bet_Point (Se A B) D
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A B) D

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P55 : "Line_on (Li D C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D C) C

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P56 : "\<not> Bet_Point (Se C C) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C C) D
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C C) D

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P48
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A C D))
[PROOF STEP]
have P57 : "Def (Ang (An A D C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A C D))

goal (1 subgoal):
 1. Def (Ang (An A D C))
[PROOF STEP]
by (simp add:Tri_to_Ang Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A D C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P57
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A D C))
[PROOF STEP]
have P58 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A D C))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P18 P53 P54 P55 P56 P57 P58
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)
Line_on (Li D A) B
\<not> Bet_Point (Se A B) D
Line_on (Li D C) C
\<not> Bet_Point (Se C C) D
Def (Ang (An A D C))
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P59 : "Eq (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An B D C)) add Emp) \<and> Def (Ang (An B D C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)
Line_on (Li D A) B
\<not> Bet_Point (Se A B) D
Line_on (Li D C) C
\<not> Bet_Point (Se C C) D
Def (Ang (An A D C))
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An B D C)) add Emp) \<and> Def (Ang (An B D C))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An B D C)) add Emp) \<and> Def (Ang (An B D C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P22
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A2 D2) B1
[PROOF STEP]
have P60 : "Line_on (Li D2 A2) B1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A2 D2) B1

goal (1 subgoal):
 1. Line_on (Li D2 A2) B1
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li D2 A2) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have "Inv (Bet_Point (Se A2 B1) D2)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Inv (Bet_Point (Se A2 B1) D2)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se A2 B1) D2)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se A2 B1) D2)
[PROOF STEP]
have P61 : "\<not> Bet_Point (Se A2 B1) D2"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se A2 B1) D2)

goal (1 subgoal):
 1. \<not> Bet_Point (Se A2 B1) D2
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A2 B1) D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P62 : "Line_on (Li D2 C2) C2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D2 C2) C2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D2 C2) C2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P63 : "\<not> Bet_Point (Se C2 C2) D2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C2 C2) D2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C2 C2) D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P49
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A2 C2 D2))
[PROOF STEP]
have P64 : "Def (Ang (An A2 D2 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A2 C2 D2))

goal (1 subgoal):
 1. Def (Ang (An A2 D2 C2))
[PROOF STEP]
by (simp add:Tri_to_Ang Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A2 D2 C2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have P65 : "\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi B1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi B1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P64
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A2 D2 C2))
[PROOF STEP]
have P66 : "\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A2 D2 C2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P60 P61 P62 P63 P64 P65 P66
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li D2 A2) B1
\<not> Bet_Point (Se A2 B1) D2
Line_on (Li D2 C2) C2
\<not> Bet_Point (Se C2 C2) D2
Def (Ang (An A2 D2 C2))
\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P67 : "Eq (Geos (Ang (An A2 D2 C2)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp) \<and> Def (Ang (An B1 D2 C2))"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li D2 A2) B1
\<not> Bet_Point (Se A2 B1) D2
Line_on (Li D2 C2) C2
\<not> Bet_Point (Se C2 C2) D2
Def (Ang (An A2 D2 C2))
\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi B1) add Emp)
\<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An A2 D2 C2)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp) \<and> Def (Ang (An B1 D2 C2))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An A2 D2 C2)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp) \<and> Def (Ang (An B1 D2 C2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P51 P59
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)
Eq (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An B D C)) add Emp) \<and> Def (Ang (An B D C))
[PROOF STEP]
have P68 : "Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)
Eq (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An B D C)) add Emp) \<and> Def (Ang (An B D C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P67 P68
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An A2 D2 C2)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp) \<and> Def (Ang (An B1 D2 C2))
Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)
[PROOF STEP]
have P69 : "Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An A2 D2 C2)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp) \<and> Def (Ang (An B1 D2 C2))
Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An A2 D2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Eq_rev Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P59
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An B D C)) add Emp) \<and> Def (Ang (An B D C))
[PROOF STEP]
have "Def (Tri (Tr B D C))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An A D C)) add Emp) (Geos (Ang (An B D C)) add Emp) \<and> Def (Ang (An B D C))

goal (1 subgoal):
 1. Def (Tri (Tr B D C))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B D C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B D C))
[PROOF STEP]
have P70 : "Def (Tri (Tr D B C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B D C))

goal (1 subgoal):
 1. Def (Tri (Tr D B C))
[PROOF STEP]
by (blast intro:Tri_def_trans Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr D B C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P67
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An A2 D2 C2)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp) \<and> Def (Ang (An B1 D2 C2))
[PROOF STEP]
have "Def (Tri (Tr B1 D2 C2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An A2 D2 C2)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp) \<and> Def (Ang (An B1 D2 C2))

goal (1 subgoal):
 1. Def (Tri (Tr B1 D2 C2))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr B1 D2 C2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B1 D2 C2))
[PROOF STEP]
have P71 : "Def (Tri (Tr D2 B1 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B1 D2 C2))

goal (1 subgoal):
 1. Def (Tri (Tr D2 B1 C2))
[PROOF STEP]
by (blast intro:Tri_def_trans Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr D2 B1 C2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have "Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp)
[PROOF STEP]
have P72 : "Eq (Geos (Seg (Se D B)) add Emp) (Geos (Seg (Se D2 B1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se D B)) add Emp) (Geos (Seg (Se D2 B1)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se D B)) add Emp) (Geos (Seg (Se D2 B1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P52 P69 P70 P71 P72
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se D C)) add Emp) (Geos (Seg (Se D2 C2)) add Emp)
Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp)
Def (Tri (Tr D B C))
Def (Tri (Tr D2 B1 C2))
Eq (Geos (Seg (Se D B)) add Emp) (Geos (Seg (Se D2 B1)) add Emp)
[PROOF STEP]
have "Cong (Geos (Tri (Tr D B C)) add Emp) (Geos (Tri (Tr D2 B1 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se D C)) add Emp) (Geos (Seg (Se D2 C2)) add Emp)
Cong (Geos (Ang (An B D C)) add Emp) (Geos (Ang (An B1 D2 C2)) add Emp)
Def (Tri (Tr D B C))
Def (Tri (Tr D2 B1 C2))
Eq (Geos (Seg (Se D B)) add Emp) (Geos (Seg (Se D2 B1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr D B C)) add Emp) (Geos (Tri (Tr D2 B1 C2)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr D B C)) add Emp) (Geos (Tri (Tr D2 B1 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr D B C)) add Emp) (Geos (Tri (Tr D2 B1 C2)) add Emp)
[PROOF STEP]
have P73 : "Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C2 B1 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr D B C)) add Emp) (Geos (Tri (Tr D2 B1 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C2 B1 D2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C2 B1 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P71
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr D2 B1 C2))
[PROOF STEP]
have "Def (Tri (Tr C2 B1 D2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr D2 B1 C2))

goal (1 subgoal):
 1. Def (Tri (Tr C2 B1 D2))
[PROOF STEP]
by (blast intro:Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C2 B1 D2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 B1 D2))
[PROOF STEP]
have P74 : "Def (Ang (An C2 B1 D2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 B1 D2))

goal (1 subgoal):
 1. Def (Ang (An C2 B1 D2))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C2 B1 D2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have P75 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P71
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr D2 B1 C2))
[PROOF STEP]
have P76 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr D2 B1 C2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P2 P75 P76
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P77 : "Line_on (Li B1 C2) C1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Line_on (Li B1 C2) C1
[PROOF STEP]
by (simp add:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C2) C1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P14
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
have P78 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P74
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C2 B1 D2))
[PROOF STEP]
have P79 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C2 B1 D2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20 P78 P79
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have P80 : "Line_on (Li B1 D2) D1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Line_on (Li B1 D2) D1
[PROOF STEP]
by (simp add:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 D2) D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have "\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
have P81 : "\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li B1 A1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li B1 A1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li B1 A1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P82 : "Line_on (Li A1 D1) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 D1) D1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 D1) D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P9 P11 P13 P14 P82
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A1 D1) B1
Line_on (Li B1 A1) D1
Line_on (Li B1 A1) B1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)
Line_on (Li A1 D1) D1
[PROOF STEP]
have P83 : "Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A1 D1) B1
Line_on (Li B1 A1) D1
Line_on (Li B1 A1) B1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)
Line_on (Li A1 D1) D1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P81 P83
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li B1 A1)) add Emp)
Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
have P84 : "\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li B1 A1)) add Emp)
Eq (Geos (Lin (Li B1 A1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
by (simp add:Eq_not_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
[PROOF STEP]
have P85 : "\<not> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P86 : "Line_on (Li B1 C1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 C1) B1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 C1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms P85 P86
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
\<not> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Line_on (Li B1 C1) B1
[PROOF STEP]
have P87 : "Plane_diffside (Li B1 C1) A1 D1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
\<not> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Line_on (Li B1 C1) B1

goal (1 subgoal):
 1. Plane_diffside (Li B1 C1) A1 D1
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B1 C1) A1 D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B1 C1) A1 D1
[PROOF STEP]
have P88 : "Plane_diffside (Li B1 C1) D1 A1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B1 C1) A1 D1

goal (1 subgoal):
 1. Plane_diffside (Li B1 C1) D1 A1
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B1 C1) D1 A1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P89 : "Bet_Point (Se D2 D1) B1 \<Longrightarrow> Line_on (Li D2 D1) B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> Line_on (Li D2 D1) B1
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Line_on (Li D2 D1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P90 : "Line_on (Li D2 D1) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D2 D1) D1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D2 D1) D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P9 P14 P82 P89 P90
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A1 D1) B1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)
Line_on (Li A1 D1) D1
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Line_on (Li D2 D1) B1
Line_on (Li D2 D1) D1
[PROOF STEP]
have P91 : "Bet_Point (Se D2 D1) B1 \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A1 D1) B1
\<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi B1) add Emp)
Line_on (Li A1 D1) D1
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Line_on (Li D2 D1) B1
Line_on (Li D2 D1) D1

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P84 P91
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)
[PROOF STEP]
have "Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)
[PROOF STEP]
by (simp add:Eq_not_trans)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)
[PROOF STEP]
have P92 : "Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D2 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li D2 D1)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D2 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D2 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P86 P92
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) B1
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D2 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
have "Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D2 D1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) B1
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D2 D1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D2 D1
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D2 D1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D2 D1
[PROOF STEP]
have P93 : "Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D1 D2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D2 D1

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D1 D2
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D1 D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have "Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A1 A2) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A1 A2) B1
[PROOF STEP]
by (blast intro:Bet_Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A1 A2) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A1 A2) B1
[PROOF STEP]
have P94 : "Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A2 A1) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A1 A2) B1

goal (1 subgoal):
 1. Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A2 A1) B1
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A2 A1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P1 P94
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A2 A1) B1
[PROOF STEP]
have P95 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
Eq (Geos (Poi D2) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> Bet_Point (Se A2 A1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P88 P93 P95
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B1 C1) D1 A1
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D1 D2
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have "Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) A1 D2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B1 C1) D1 A1
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D1 D2
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) A1 D2
[PROOF STEP]
by (blast intro:Plane_trans_inv)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) A1 D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) A1 D2
[PROOF STEP]
have P96 : "Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) D2 A1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) A1 D2

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) D2 A1
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) D2 A1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
[PROOF STEP]
have "Def (Tri (Tr A2 B1 C1))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))

goal (1 subgoal):
 1. Def (Tri (Tr A2 B1 C1))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A2 B1 C1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A2 B1 C1))
[PROOF STEP]
have P97 : "\<not> Line_on (Li B1 C1) A2"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A2 B1 C1))

goal (1 subgoal):
 1. \<not> Line_on (Li B1 C1) A2
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B1 C1) A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have "Line_on (Li D2 A2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D2 A2) A2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D2 A2) A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li D2 A2) A2
[PROOF STEP]
have P98 : "Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li D2 A2) A2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A2
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P97 P98
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B1 C1) A2
Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A2
[PROOF STEP]
have P99 : "\<not> Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B1 C1) A2
Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp) \<Longrightarrow> Line_on (Li B1 C1) A2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have P100 : "Bet_Point (Se D2 A2) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se B1 D2)) add Emp) \<and> Bet_Point (Se D2 A2) B1 \<and> Line_on (Li B1 D1) D2 \<and> \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se D2 A2) B1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 A2) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P86 P99 P100
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) B1
\<not> Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Bet_Point (Se D2 A2) B1
[PROOF STEP]
have P101 : "Plane_diffside (Li B1 C1) D2 A2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) B1
\<not> Eq (Geos (Lin (Li D2 A2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
Bet_Point (Se D2 A2) B1

goal (1 subgoal):
 1. Plane_diffside (Li B1 C1) D2 A2
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B1 C1) D2 A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P96 P101
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) D2 A1
Plane_diffside (Li B1 C1) D2 A2
[PROOF STEP]
have "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se D2 D1) B1 \<Longrightarrow>
    Plane_diffside (Li B1 C1) A1 A2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_sameside (Li B1 C1) D2 A1
Plane_diffside (Li B1 C1) D2 A2

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_diffside (Li B1 C1) A1 A2
[PROOF STEP]
by (simp add:Plane_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_diffside (Li B1 C1) A1 A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_diffside (Li B1 C1) A1 A2
[PROOF STEP]
have P102 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se D2 D1) B1 \<Longrightarrow>
    \<not> Plane_sameside (Li B1 C1) A1 A2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_diffside (Li B1 C1) A1 A2

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) A1 A2
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) A1 A2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P103 : "Line_on (Li B1 A1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B1 A1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B1 A1) A1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have "Def (Tri (Tr C1 B1 A1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. Def (Tri (Tr C1 B1 A1))
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C1 B1 A1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C1 B1 A1))
[PROOF STEP]
have P104 : "\<not> Line_on (Li B1 A1) C1"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C1 B1 A1))

goal (1 subgoal):
 1. \<not> Line_on (Li B1 A1) C1
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B1 A1) C1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B1 A2 C2))
[PROOF STEP]
have P105 : "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B1 A2 C2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
by (simp add:Tri_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P1 p10 P13 P103 P104 P105
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li B1 A1) B1
Line_on (Li B1 A1) A1
\<not> Line_on (Li B1 A1) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P106 : "Plane_sameside (Li C1 B1) A2 A1 \<or> Eq (Geos (Poi A2) add Emp) (Geos (Poi A1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C1)) add Emp) \<and> Eq (Geos (Seg (Se B A)) add Emp) (Geos (Seg (Se B1 A2)) add Emp) \<and> Line_on (Li B1 A1) A2 \<and> \<not> Bet_Point (Se A2 A1) B1 \<and> Def (Ang (An A2 B1 C1))
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
Line_on (Li B1 A1) B1
Line_on (Li B1 A1) A1
\<not> Line_on (Li B1 A1) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li C1 B1) A2 A1 \<or> Eq (Geos (Poi A2) add Emp) (Geos (Poi A1) add Emp)
[PROOF STEP]
by (simp add:Seg_Plane_sameside)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C1 B1) A2 A1 \<or> Eq (Geos (Poi A2) add Emp) (Geos (Poi A1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1
[PROOF STEP]
have "\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Def (Ang (An A1 B1 C1))
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Bet_Point (Se A D) B
Bet_Point (Se A1 D1) B1

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
[PROOF STEP]
have P107 : "Eq (Geos (Lin (Li C1 B1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li C1 B1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
by (simp add:Line_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li C1 B1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P106 P107
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li C1 B1) A2 A1 \<or> Eq (Geos (Poi A2) add Emp) (Geos (Poi A1) add Emp)
Eq (Geos (Lin (Li C1 B1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
have P108 : "Plane_sameside (Li B1 C1) A1 A2 \<or> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li C1 B1) A2 A1 \<or> Eq (Geos (Poi A2) add Emp) (Geos (Poi A1) add Emp)
Eq (Geos (Lin (Li C1 B1)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li B1 C1) A1 A2 \<or> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
by (blast intro:Plane_sameside_rev Plane_Line_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li B1 C1) A1 A2 \<or> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P102 P108
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) A1 A2
Plane_sameside (Li B1 C1) A1 A2 \<or> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P109 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) A1 A2
Plane_sameside (Li B1 C1) A1 A2 \<or> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P22
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A2 D2) B1
[PROOF STEP]
have P110 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se A1 D2) B1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A2 D2) B1

goal (1 subgoal):
 1. Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se A1 D2) B1
[PROOF STEP]
by (blast intro:Bet_Point_Eq Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se A1 D2) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se A1 D2) B1
[PROOF STEP]
have P111 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Line_on (Li A1 D2) B1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se A1 D2) B1

goal (1 subgoal):
 1. Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Line_on (Li A1 D2) B1
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Line_on (Li A1 D2) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P112 : "Line_on (Li A1 D2) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 D2) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 D2) A1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have P113 : "Line_on (Li A1 D1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A1 D1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A1 D1) A1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from p10
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)
[PROOF STEP]
have P114 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi A1) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P9 P111 P112 P113 P114
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A1 D1) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Line_on (Li A1 D2) B1
Line_on (Li A1 D2) A1
Line_on (Li A1 D1) A1
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
have P115 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A1 D1) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Line_on (Li A1 D2) B1
Line_on (Li A1 D2) A1
Line_on (Li A1 D1) A1
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P84 P115
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)
[PROOF STEP]
have "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D1)) add Emp)
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A1 D1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)
[PROOF STEP]
by (simp add:Eq_not_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)
[PROOF STEP]
have P116 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li A1 D2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B1 C1)) add Emp) (Geos (Lin (Li A1 D2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li A1 D2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li A1 D2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P86 P110 P116
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B1 C1) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se A1 D2) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li A1 D2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)
[PROOF STEP]
have P117 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Plane_diffside (Li B1 C1) A1 D2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B1 C1) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se A1 D2) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Eq (Geos (Lin (Li A1 D2)) add Emp) (Geos (Lin (Li B1 C1)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Plane_diffside (Li B1 C1) A1 D2
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Plane_diffside (Li B1 C1) A1 D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
have "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi D1) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
have P118 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se D2 D1) B1 \<Longrightarrow>
    \<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi D2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D2) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P87 P117 P118
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B1 C1) A1 D1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Plane_diffside (Li B1 C1) A1 D2
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi D2) add Emp)
[PROOF STEP]
have P119 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Bet_Point (Se D2 D1) B1 \<Longrightarrow>
    Plane_sameside (Li B1 C1) D1 D2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B1 C1) A1 D1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> Plane_diffside (Li B1 C1) A1 D2
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D1) add Emp) (Geos (Poi D2) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_sameside (Li B1 C1) D1 D2
[PROOF STEP]
by (blast intro:Plane_trans_inv)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_sameside (Li B1 C1) D1 D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P93
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D1 D2
[PROOF STEP]
have P120 : "Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) D1 D2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> Plane_diffside (Li B1 C1) D1 D2

goal (1 subgoal):
 1. Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) D1 D2
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) D1 D2

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P119 P120
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_sameside (Li B1 C1) D1 D2
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) D1 D2
[PROOF STEP]
have P121 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp); Bet_Point (Se D2 D1) B1\<rbrakk> \<Longrightarrow> Plane_sameside (Li B1 C1) D1 D2
Bet_Point (Se D2 D1) B1 \<Longrightarrow> \<not> Plane_sameside (Li B1 C1) D1 D2

goal (1 subgoal):
 1. Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P109 P121
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1
[PROOF STEP]
have P122 : "\<not> Bet_Point (Se D2 D1) B1"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1
Eq (Geos (Poi A1) add Emp) (Geos (Poi A2) add Emp) \<Longrightarrow> \<not> Bet_Point (Se D2 D1) B1

goal (1 subgoal):
 1. \<not> Bet_Point (Se D2 D1) B1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se D2 D1) B1

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P2 P74 P75 P77 P78 P80 P122
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))
Def (Ang (An C2 B1 D2))
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B1 C2) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 D2) D1
\<not> Bet_Point (Se D2 D1) B1
[PROOF STEP]
have P123 : "Eq (Geos (Ang (An C2 B1 D2)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An A2 B1 C2)) add Emp) \<and> Eq (Geos (Seg (Se B C)) add Emp) (Geos (Seg (Se B1 C2)) add Emp) \<and> Line_on (Li B1 C1) C2 \<and> \<not> Bet_Point (Se C2 C1) B1 \<and> Def (Ang (An A2 B1 C2))
Def (Ang (An C2 B1 D2))
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B1 C2) C1
\<not> Eq (Geos (Poi B1) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B1 D2) D1
\<not> Bet_Point (Se D2 D1) B1

goal (1 subgoal):
 1. Eq (Geos (Ang (An C2 B1 D2)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C2 B1 D2)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
from P73 P123
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C2 B1 D2)) add Emp)
Eq (Geos (Ang (An C2 B1 D2)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C2 B1 D2)) add Emp)
Eq (Geos (Ang (An C2 B1 D2)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An C1 B1 D1)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed