[STATEMENT]
theorem (in Congruence_Rule) Tri_SSS :
  assumes
    "Def (Tri (Tr A1 B1 C1))" "Def (Tri (Tr A2 B2 C2))"
    "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)"
    "Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)"
    "Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)"
  shows "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have "Def (Tri (Tr C2 B2 A2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr C2 B2 A2))
[PROOF STEP]
have P1 : "\<not> Line_on (Li A2 C2) B2"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr C2 B2 A2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P2 : "Def (Ang (An B1 A1 C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

goal (1 subgoal):
 1. Def (Ang (An B1 A1 C1))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B1 A1 C1))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P1 P2
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A2 C2) B2
Def (Ang (An B1 A1 C1))
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) p B2"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A2 C2) B2
Def (Ang (An B1 A1 C1))

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) p B2
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) p B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) p B2
[PROOF STEP]
obtain B21 :: Point where P3 : "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp)
    \<and> Plane_sameside (Li A2 C2) B21 B2"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) p B2

goal (1 subgoal):
 1. (\<And>B21. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2
[PROOF STEP]
have P4 : "\<not> Line_on (Li A2 C2) B21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P2 P4
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B1 A1 C1))
\<not> Line_on (Li A2 C2) B21
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) p B21"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B1 A1 C1))
\<not> Line_on (Li A2 C2) B21

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) p B21
[PROOF STEP]
by (simp add:Ang_move_diffside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) p B21

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) p B21
[PROOF STEP]
obtain B22 :: Point where P5 : "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp)
    \<and> Plane_diffside (Li A2 C2) B22 B21"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An p A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) p B21

goal (1 subgoal):
 1. (\<And>B22. Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li A2 B21) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 B21) A2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B21) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P7 : "Line_on (Li A2 B21) B21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 B21) B21
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B21) B21

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P8 : "Line_on (Li A2 C2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 C2) A2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 C2) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 C2) A2
[PROOF STEP]
have P9 : "Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp) \<Longrightarrow> Line_on (Li A2 C2) B21"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 C2) A2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P4 P9
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A2 C2) B21
Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp) \<Longrightarrow> Line_on (Li A2 C2) B21
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A2 C2) B21
Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp) \<Longrightarrow> Line_on (Li A2 C2) B21

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P11 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6 P7 P10 P11
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 B21) A2
Line_on (Li A2 B21) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp)
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 p)) add Emp)
    \<and> \<not> Bet_Point (Se p B21) A2 \<and> Line_on (Li A2 B21) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 B21) A2
Line_on (Li A2 B21) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp)
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p B21) A2 \<and> Line_on (Li A2 B21) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain B211 :: Point where P12 : "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)
    \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p B21) A2 \<and> Line_on (Li A2 B21) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P13 : "Line_on (Li A2 B22) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 B22) A2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B22) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P14 : "Line_on (Li A2 B22) B22"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 B22) B22
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B22) B22

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 C2) A2
[PROOF STEP]
have P15 : "Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp) \<Longrightarrow> Line_on (Li A2 C2) B22"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 C2) A2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21
[PROOF STEP]
have P16 : "\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p
    \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P15 P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp) \<Longrightarrow> Line_on (Li A2 C2) B22
\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp) \<Longrightarrow> Line_on (Li A2 C2) B22
\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P11 P13 P14 P17
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
Line_on (Li A2 B22) A2
Line_on (Li A2 B22) B22
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 p)) add Emp)
    \<and> \<not> Bet_Point (Se p B22) A2 \<and> Line_on (Li A2 B22) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi B1) add Emp)
Line_on (Li A2 B22) A2
Line_on (Li A2 B22) B22
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p B22) A2 \<and> Line_on (Li A2 B22) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain B221 :: Point where P18 : "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp)
    \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 p)) add Emp) \<and> \<not> Bet_Point (Se p B22) A2 \<and> Line_on (Li A2 B22) p \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi p) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P19 : "\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) 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 P20 : "\<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 (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P4 P20
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A2 C2) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P21 : "Def (Ang (An B21 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A2 C2) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Def (Ang (An B21 A2 C2))
[PROOF STEP]
by (blast intro:Ang_sinple_def Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B21 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
[PROOF STEP]
have "\<not> Bet_Point (Se B211 B21) A2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)

goal (1 subgoal):
 1. \<not> Bet_Point (Se B211 B21) A2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B211 B21) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se B211 B21) A2
[PROOF STEP]
have P22 : "\<not> Bet_Point (Se B21 B211) A2"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se B211 B21) A2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P23 : "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 (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P24 : "\<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 (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P12 P20 P21 P22 P23 P24
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Def (Ang (An B21 A2 C2))
\<not> Bet_Point (Se B21 B211) A2
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2
[PROOF STEP]
have P25 :
    "Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Def (Ang (An B21 A2 C2))
\<not> Bet_Point (Se B21 B211) A2
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P3 P25
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))
[PROOF STEP]
have P26 : "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P27 : "Def (Tri (Tr A1 B1 C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P25
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))
[PROOF STEP]
have P28 : "Def (Tri (Tr A2 B211 C2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P29 : "Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P12 P26 P27 P28 P29
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B211 C2))
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
have "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B211 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B211 C2))
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B211 C2)) add Emp)
[PROOF STEP]
have P30 : "Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B211 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P16 P20
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P31 : "Def (Ang (An B22 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Def (Ang (An B22 A2 C2))
[PROOF STEP]
by (blast intro:Ang_sinple_def Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B22 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P18
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
[PROOF STEP]
have "\<not> Bet_Point (Se B221 B22) A2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)

goal (1 subgoal):
 1. \<not> Bet_Point (Se B221 B22) A2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B221 B22) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se B221 B22) A2
[PROOF STEP]
have P32 : "\<not> Bet_Point (Se B22 B221) A2"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se B221 B22) A2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P18 P20 P23 P24 P31 P32
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2
Def (Ang (An B22 A2 C2))
\<not> Bet_Point (Se B22 B221) A2
[PROOF STEP]
have P33 :
    "Eq (Geos (Ang (An B22 A2 C2)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp) \<and> Def (Ang (An B221 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2
Def (Ang (An B22 A2 C2))
\<not> Bet_Point (Se B22 B221) A2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P5 P33
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21
Eq (Geos (Ang (An B22 A2 C2)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp) \<and> Def (Ang (An B221 A2 C2))
[PROOF STEP]
have P34 : "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21
Eq (Geos (Ang (An B22 A2 C2)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp) \<and> Def (Ang (An B221 A2 C2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P33
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An B22 A2 C2)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp) \<and> Def (Ang (An B221 A2 C2))
[PROOF STEP]
have P35 : "Def (Tri (Tr A2 B221 C2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An B22 A2 C2)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp) \<and> Def (Ang (An B221 A2 C2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P18 P27 P29 P34 P35
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp)
Def (Tri (Tr A2 B221 C2))
[PROOF STEP]
have "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B221 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
Def (Tri (Tr A1 B1 C1))
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B221 A2 C2)) add Emp)
Def (Tri (Tr A2 B221 C2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B221 C2)) add Emp)
[PROOF STEP]
have P36 : "Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B221 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B221 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
[PROOF STEP]
have P37 : "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P18
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
[PROOF STEP]
have P38 : "Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P37 P38
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp)
[PROOF STEP]
have P39 : "Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P38
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp)
[PROOF STEP]
have P40 : "Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P30 P36
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B221 C2)) add Emp)
[PROOF STEP]
have P41 : "Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B221 C2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P36
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B221 C2)) add Emp)
[PROOF STEP]
have P42 : "Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B221 C2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21
[PROOF STEP]
have P43 : "Plane_diffside (Li A2 C2) B22 B21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B22 A2 C2)) add Emp) \<and> Plane_diffside (Li A2 C2) B22 B21

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B22 B21
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B22 B21

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B22 B21
[PROOF STEP]
have P44 : "Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow>
    Plane_diffside (Li A2 C2) B22 B211"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B22 B21

goal (1 subgoal):
 1. Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211
[PROOF STEP]
by (blast intro:Point_Eq Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6 P8 P20 P23
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 B21) A2
Line_on (Li A2 C2) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2
[PROOF STEP]
have P45 : "Line_on (Li A2 B21) C2 \<Longrightarrow>
    Eq (Geos (Lin (Li A2 B21)) add Emp) (Geos (Lin (Li A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 B21) A2
Line_on (Li A2 C2) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P7 P45
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 B21) B21
Line_on (Li A2 B21) C2 \<Longrightarrow> Eq (Geos (Lin (Li A2 B21)) add Emp) (Geos (Lin (Li A2 C2)) add Emp)
[PROOF STEP]
have P46 : "Line_on (Li A2 B21) C2 \<Longrightarrow> Line_on (Li A2 C2) B21"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 B21) B21
Line_on (Li A2 B21) C2 \<Longrightarrow> Eq (Geos (Lin (Li A2 B21)) add Emp) (Geos (Lin (Li A2 C2)) add Emp)

goal (1 subgoal):
 1. Line_on (Li A2 B21) C2 \<Longrightarrow> Line_on (Li A2 C2) B21
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B21) C2 \<Longrightarrow> Line_on (Li A2 C2) B21

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P4 P46
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A2 C2) B21
Line_on (Li A2 B21) C2 \<Longrightarrow> Line_on (Li A2 C2) B21
[PROOF STEP]
have P47 : "\<not> Line_on (Li A2 B21) C2"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A2 C2) B21
Line_on (Li A2 B21) C2 \<Longrightarrow> Line_on (Li A2 C2) B21

goal (1 subgoal):
 1. \<not> Line_on (Li A2 B21) C2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A2 B21) C2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P6 P7 P10 P12 P22 P47
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 B21) A2
Line_on (Li A2 B21) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
\<not> Bet_Point (Se B21 B211) A2
\<not> Line_on (Li A2 B21) C2
[PROOF STEP]
have P48 : "Plane_sameside (Li C2 A2) B21 B211 \<or> Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 B21) A2
Line_on (Li A2 B21) B21
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B21) add Emp)
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
\<not> Bet_Point (Se B21 B211) A2
\<not> Line_on (Li A2 B21) C2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P49 : "Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow>
    Plane_sameside (Li A2 C2) B21 B211"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_sameside (Li A2 C2) B21 B211
[PROOF STEP]
by (blast intro:Line_rev Plane_Line_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_sameside (Li A2 C2) B21 B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P43
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B22 B21
[PROOF STEP]
have P50 : "Plane_diffside (Li A2 C2) B21 B22"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B22 B21

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B21 B22
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B21 B22

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P49 P50
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_sameside (Li A2 C2) B21 B211
Plane_diffside (Li A2 C2) B21 B22
[PROOF STEP]
have P51 : "Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow>
    Plane_diffside (Li A2 C2) B22 B211"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_sameside (Li A2 C2) B21 B211
Plane_diffside (Li A2 C2) B21 B22

goal (1 subgoal):
 1. Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211
[PROOF STEP]
by (simp add:Plane_trans Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P44 P48 P51
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211
Plane_sameside (Li C2 A2) B21 B211 \<or> Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp)
Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211
[PROOF STEP]
have P52 : "Plane_diffside (Li A2 C2) B22 B211"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211
Plane_sameside (Li C2 A2) B21 B211 \<or> Eq (Geos (Poi B21) add Emp) (Geos (Poi B211) add Emp)
Plane_sameside (Li C2 A2) B21 B211 \<Longrightarrow> Plane_diffside (Li A2 C2) B22 B211

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B22 B211
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B22 B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B22 B211
[PROOF STEP]
have "Plane_diffside (Li A2 C2) B211 B22"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B22 B211

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B211 B22
[PROOF STEP]
by (blast intro:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B211 B22

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B211 B22
[PROOF STEP]
have P53 : "Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow>
    Plane_diffside (Li A2 C2) B211 B221"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B211 B22

goal (1 subgoal):
 1. Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221
[PROOF STEP]
by (blast intro:Point_Eq Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P8 P13 P20 P23
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 C2) A2
Line_on (Li A2 B22) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2
[PROOF STEP]
have P54 : "Line_on (Li A2 B22) C2 \<Longrightarrow>
    Eq (Geos (Lin (Li A2 B22)) add Emp) (Geos (Lin (Li A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 C2) A2
Line_on (Li A2 B22) A2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P14 P54
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 B22) B22
Line_on (Li A2 B22) C2 \<Longrightarrow> Eq (Geos (Lin (Li A2 B22)) add Emp) (Geos (Lin (Li A2 C2)) add Emp)
[PROOF STEP]
have P55 : "Line_on (Li A2 B22) C2 \<Longrightarrow> Line_on (Li A2 C2) B22"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 B22) B22
Line_on (Li A2 B22) C2 \<Longrightarrow> Eq (Geos (Lin (Li A2 B22)) add Emp) (Geos (Lin (Li A2 C2)) add Emp)

goal (1 subgoal):
 1. Line_on (Li A2 B22) C2 \<Longrightarrow> Line_on (Li A2 C2) B22
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B22) C2 \<Longrightarrow> Line_on (Li A2 C2) B22

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P16 P55
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21
Line_on (Li A2 B22) C2 \<Longrightarrow> Line_on (Li A2 C2) B22
[PROOF STEP]
have P56 : "\<not> Line_on (Li A2 B22) C2"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se B22 B21) p \<and> Line_on (Li A2 C2) p \<and> \<not> Line_on (Li A2 C2) B22 \<and> \<not> Line_on (Li A2 C2) B21
Line_on (Li A2 B22) C2 \<Longrightarrow> Line_on (Li A2 C2) B22

goal (1 subgoal):
 1. \<not> Line_on (Li A2 B22) C2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A2 B22) C2

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

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B22) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P57 : "\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B22) add Emp) (Geos (Poi A2) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P13 P14 P18 P32 P56 P57
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 B22) A2
Line_on (Li A2 B22) B22
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
\<not> Bet_Point (Se B22 B221) A2
\<not> Line_on (Li A2 B22) C2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp)
[PROOF STEP]
have P58 : "Plane_sameside (Li C2 A2) B22 B221 \<or> Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 B22) A2
Line_on (Li A2 B22) B22
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B221)) add Emp) \<and> \<not> Bet_Point (Se B221 B22) A2 \<and> Line_on (Li A2 B22) B221 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B221) add Emp)
\<not> Bet_Point (Se B22 B221) A2
\<not> Line_on (Li A2 B22) C2
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B22) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P20
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
[PROOF STEP]
have P59 : "Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_sameside (Li A2 C2) B22 B221"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_sameside (Li A2 C2) B22 B221
[PROOF STEP]
by (blast intro:Line_rev Plane_Line_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_sameside (Li A2 C2) B22 B221

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P52 P59
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B22 B211
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_sameside (Li A2 C2) B22 B221
[PROOF STEP]
have P60 : "Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow>
    Plane_diffside (Li A2 C2) B211 B221"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B22 B211
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_sameside (Li A2 C2) B22 B221

goal (1 subgoal):
 1. Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221
[PROOF STEP]
by (simp add:Plane_trans Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P53 P58 P60
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221
Plane_sameside (Li C2 A2) B22 B221 \<or> Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp)
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221
[PROOF STEP]
have "Plane_diffside (Li A2 C2) B211 B221"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221
Plane_sameside (Li C2 A2) B22 B221 \<or> Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp)
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B211 B221

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B211 B221
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B211 B221

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B211 B221
[PROOF STEP]
have P61 : "Plane_diffside (Li A2 C2) B221 B211"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B211 B221

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B221 B211
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B221 B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P20 P61
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Plane_diffside (Li A2 C2) B221 B211
[PROOF STEP]
have P62 : "Plane_diffside (Li C2 A2) B221 B211"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Plane_diffside (Li A2 C2) B221 B211

goal (1 subgoal):
 1. Plane_diffside (Li C2 A2) B221 B211
[PROOF STEP]
by (blast intro:Line_rev Plane_Line_diff_trans)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li C2 A2) B221 B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P63 : "Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P64 : "Eq (Geos (Seg (Se B211 C2)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B211 C2)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B211 C2)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P41 P63 P64
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)
Eq (Geos (Seg (Se B211 C2)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)
[PROOF STEP]
have P65 : "Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B211 C2)) add Emp)
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)
Eq (Geos (Seg (Se B211 C2)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P19 P39 P62 P65
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)
Plane_diffside (Li C2 A2) B221 B211
Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)
[PROOF STEP]
have P66 : "Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B211)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B211)) add Emp)
Plane_diffside (Li C2 A2) B221 B211
Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B211)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B211)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_SSS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B211)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P67 : "Eq (Geos (Ang (An C2 A2 B211)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An C2 A2 B211)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C2 A2 B211)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P66 P67
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B211)) add Emp)
Eq (Geos (Ang (An C2 A2 B211)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)
[PROOF STEP]
have P68 : "Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B211)) add Emp)
Eq (Geos (Ang (An C2 A2 B211)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2
[PROOF STEP]
have P69 : "Plane_sameside (Li A2 C2) B21 B2"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2

goal (1 subgoal):
 1. Plane_sameside (Li A2 C2) B21 B2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li A2 C2) B21 B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P50 P69
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B21 B22
Plane_sameside (Li A2 C2) B21 B2
[PROOF STEP]
have P70 : "Plane_diffside (Li A2 C2) B2 B22"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B21 B22
Plane_sameside (Li A2 C2) B21 B2

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B2 B22
[PROOF STEP]
by (simp add:Plane_trans)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B2 B22

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B2 B22
[PROOF STEP]
have P71 : "Plane_diffside (Li A2 C2) B22 B2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B2 B22

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B22 B2
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B22 B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P70
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B2 B22
[PROOF STEP]
have P72 : "Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow>
    Plane_diffside (Li A2 C2) B221 B2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B2 B22

goal (1 subgoal):
 1. Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2
[PROOF STEP]
by (blast intro:Point_Eq Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P59 P71
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_sameside (Li A2 C2) B22 B221
Plane_diffside (Li A2 C2) B22 B2
[PROOF STEP]
have P73 : "Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow>
    Plane_diffside (Li A2 C2) B221 B2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_sameside (Li A2 C2) B22 B221
Plane_diffside (Li A2 C2) B22 B2

goal (1 subgoal):
 1. Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2
[PROOF STEP]
by (simp add:Plane_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P58 P72 P73
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li C2 A2) B22 B221 \<or> Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp)
Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2
[PROOF STEP]
have P74 : "Plane_diffside (Li A2 C2) B221 B2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li C2 A2) B22 B221 \<or> Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp)
Eq (Geos (Poi B22) add Emp) (Geos (Poi B221) add Emp) \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2
Plane_sameside (Li C2 A2) B22 B221 \<Longrightarrow> Plane_diffside (Li A2 C2) B221 B2

goal (1 subgoal):
 1. Plane_diffside (Li A2 C2) B221 B2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li A2 C2) B221 B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P20 P74
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Plane_diffside (Li A2 C2) B221 B2
[PROOF STEP]
have P75 : "Plane_diffside (Li C2 A2) B221 B2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Plane_diffside (Li A2 C2) B221 B2

goal (1 subgoal):
 1. Plane_diffside (Li C2 A2) B221 B2
[PROOF STEP]
by (blast intro:Line_rev Plane_Line_diff_trans)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li C2 A2) B221 B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P76 : "Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P77 : "Eq (Geos (Seg (Se B2 C2)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B2 C2)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B2 C2)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P42 P76 P77
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)
Eq (Geos (Seg (Se B2 C2)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)
[PROOF STEP]
have P78 : "Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se B221 C2)) add Emp) (Geos (Seg (Se C2 B221)) add Emp)
Eq (Geos (Seg (Se B2 C2)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P19 P40 P75 P78
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Plane_diffside (Li C2 A2) B221 B2
Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)
[PROOF STEP]
have P79 : "Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C2) add Emp) (Geos (Poi A2) add Emp)
Eq (Geos (Seg (Se A2 B221)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Plane_diffside (Li C2 A2) B221 B2
Eq (Geos (Seg (Se C2 B221)) add Emp) (Geos (Seg (Se C2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_SSS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P80 : "Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P79 P80
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P81 : "Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An C2 A2 B2)) add Emp)
Eq (Geos (Ang (An C2 A2 B2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P52 P71
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li A2 C2) B22 B211
Plane_diffside (Li A2 C2) B22 B2
[PROOF STEP]
have P82 : "\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow>
    Plane_sameside (Li A2 C2) B2 B211"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li A2 C2) B22 B211
Plane_diffside (Li A2 C2) B22 B2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P68 P81 P82
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Plane_sameside (Li A2 C2) B2 B211
[PROOF STEP]
have P83 : "\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li B211 A2)) add Emp) \<and> \<not> Bet_Point (Se B2 B211) A2"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp)
Cong (Geos (Ang (An C2 A2 B221)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Plane_sameside (Li A2 C2) B2 B211

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li B211 A2)) add Emp) \<and> \<not> Bet_Point (Se B2 B211) A2
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li B211 A2)) add Emp) \<and> \<not> Bet_Point (Se B2 B211) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P84 : "Def (Ang (An B2 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

goal (1 subgoal):
 1. Def (Ang (An B2 A2 C2))
[PROOF STEP]
by (blast intro:Tri_to_Ang Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B2 A2 C2))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B2 A2 C2))
[PROOF STEP]
have "\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi A2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B2 A2 C2))

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi A2) add Emp)
[PROOF STEP]
have P85 : "Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li A2 B2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi A2) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P86 : "Line_on (Li B211 A2) B211"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B211 A2) B211
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B211 A2) B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P83 P85 P86
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li B211 A2)) add Emp) \<and> \<not> Bet_Point (Se B2 B211) A2
Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li A2 B2)) add Emp)
Line_on (Li B211 A2) B211
[PROOF STEP]
have P87 : "\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow>
    Line_on (Li A2 B2) B211"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li B211 A2)) add Emp) \<and> \<not> Bet_Point (Se B2 B211) A2
Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li A2 B2)) add Emp)
Line_on (Li B211 A2) B211

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have "Line_on (Li A2 B2) B2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A2 B2) B2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B2) B2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A2 B2) B2
[PROOF STEP]
have P88 : "Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Line_on (Li A2 B2) B211"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A2 B2) B2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P87 P88
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Line_on (Li A2 B2) B211
Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Line_on (Li A2 B2) B211
[PROOF STEP]
have P89 : "Line_on (Li A2 B2) B211"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Line_on (Li A2 B2) B211
Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Line_on (Li A2 B2) B211

goal (1 subgoal):
 1. Line_on (Li A2 B2) B211
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on (Li A2 B2) B211

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P90 : "\<not> Bet_Point (Se B2 B2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se B2 B2) A2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B2 B2) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P91 : "Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow>
    Bet_Point (Se B211 B2) A2 \<Longrightarrow> Bet_Point (Se B2 B2) A2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp); Bet_Point (Se B211 B2) A2\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) A2
[PROOF STEP]
by (blast intro:Eq_rev Bet_Point_Eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp); Bet_Point (Se B211 B2) A2\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P90 P91
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se B2 B2) A2
\<lbrakk>Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp); Bet_Point (Se B211 B2) A2\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) A2
[PROOF STEP]
have P92 : "Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B2 B211) A2"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se B2 B2) A2
\<lbrakk>Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp); Bet_Point (Se B211 B2) A2\<rbrakk> \<Longrightarrow> Bet_Point (Se B2 B2) A2

goal (1 subgoal):
 1. Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B2 B211) A2
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B2 B211) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P83 P92
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li B211 A2)) add Emp) \<and> \<not> Bet_Point (Se B2 B211) A2
Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B2 B211) A2
[PROOF STEP]
have P93 : "\<not> Bet_Point (Se B2 B211) A2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B2 A2)) add Emp) (Geos (Lin (Li B211 A2)) add Emp) \<and> \<not> Bet_Point (Se B2 B211) A2
Eq (Geos (Poi B2) add Emp) (Geos (Poi B211) add Emp) \<Longrightarrow> \<not> Bet_Point (Se B2 B211) A2

goal (1 subgoal):
 1. \<not> Bet_Point (Se B2 B211) A2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se B2 B211) A2

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P12 P20 P23 P24 P84 P89 P93
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2
Def (Ang (An B2 A2 C2))
Line_on (Li A2 B2) B211
\<not> Bet_Point (Se B2 B211) A2
[PROOF STEP]
have P94 :
    "Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B211)) add Emp) \<and> \<not> Bet_Point (Se B211 B21) A2 \<and> Line_on (Li A2 B21) B211 \<and> \<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi B211) add Emp)
\<not> Eq (Geos (Poi A2) add Emp) (Geos (Poi C2) add Emp)
Line_on (Li A2 C2) C2
\<not> Bet_Point (Se C2 C2) A2
Def (Ang (An B2 A2 C2))
Line_on (Li A2 B2) B211
\<not> Bet_Point (Se B2 B211) A2

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P25 P94
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))
Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))
[PROOF STEP]
have P95 : "Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))
Eq (Geos (Ang (An B2 A2 C2)) add Emp) (Geos (Ang (An B211 A2 C2)) add Emp) \<and> Def (Ang (An B211 A2 C2))

goal (1 subgoal):
 1. Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from P3 P95
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
[PROOF STEP]
have P96 : "Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B21 A2 C2)) add Emp) \<and> Plane_sameside (Li A2 C2) B21 B2
Eq (Geos (Ang (An B21 A2 C2)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P97 : "Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
have P98 : "Eq (Geos (Seg (Se C2 A2)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se C2 A2)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C2 A2)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P97 P98
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Eq (Geos (Seg (Se C2 A2)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
have P99 : "Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se A1 C1)) add Emp)
Eq (Geos (Seg (Se C2 A2)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P100 : "Def (Tri (Tr A1 B1 C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
[PROOF STEP]
have P101 : "Def (Tri (Tr A2 B2 C2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)
[PROOF STEP]
from assms P96 P99 P100 P101
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
[PROOF STEP]
show "Cong (Geos (Tri (Tr A1 B1 C1)) add Emp) (Geos (Tri (Tr A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))
Eq (Geos (Seg (Se A1 B1)) add Emp) (Geos (Seg (Se A2 B2)) add Emp)
Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C2)) add Emp)
Eq (Geos (Seg (Se C1 A1)) add Emp) (Geos (Seg (Se C2 A2)) add Emp)
Cong (Geos (Ang (An B1 A1 C1)) add Emp) (Geos (Ang (An B2 A2 C2)) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A2 C2)) add Emp)
Def (Tri (Tr A1 B1 C1))
Def (Tri (Tr A2 B2 C2))

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

goal:
No subgoals!
[PROOF STEP]
qed