[STATEMENT]
theorem (in Congruence_Rule) Ang_trans :
  assumes
    "Def (Ang (An A1 B1 C1))" "Def (Ang (An A2 B2 C2))" "Def (Ang (An A3 B3 C3))"
    "Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)"
    "Cong (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)"
  shows "Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A1 B1 C1))
Def (Ang (An A2 B2 C2))
Def (Ang (An A3 B3 C3))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
[PROOF STEP]
have P1 : "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A2 B2 C2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A1 B1 C1))
Def (Ang (An A2 B2 C2))
Def (Ang (An A3 B3 C3))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p q. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B2 q)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An p B2 q)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 p)) add Emp) \<and> Line_on (Li B2 A2) p \<and> \<not> Bet_Point (Se p A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 q)) add Emp) \<and> Line_on (Li B2 C2) q \<and> \<not> Bet_Point (Se q C2) B2 \<and> Def (Ang (An p B2 q))
[PROOF STEP]
obtain A21 C21 :: Point where P2 : "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp)
    \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp)
    \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp)
    \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2
    \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp)
    \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p q. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B2 q)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An p B2 q)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 p)) add Emp) \<and> Line_on (Li B2 A2) p \<and> \<not> Bet_Point (Se p A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 q)) add Emp) \<and> Line_on (Li B2 C2) q \<and> \<not> Bet_Point (Se q C2) B2 \<and> Def (Ang (An p B2 q))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A1 B1 C1))
Def (Ang (An A2 B2 C2))
Def (Ang (An A3 B3 C3))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
[PROOF STEP]
have P3 : "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A1 B1 C1))
Def (Ang (An A2 B2 C2))
Def (Ang (An A3 B3 C3))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
by (simp add:Ang_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from assms P3
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A1 B1 C1))
Def (Ang (An A2 B2 C2))
Def (Ang (An A3 B3 C3))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
have "\<exists>p q. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B3 q)) add Emp)
    \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An p B3 q)) add Emp)
    \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 p)) add Emp)
    \<and> Line_on (Li B3 A3) p \<and> \<not> Bet_Point (Se p A3) B3
    \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 q)) add Emp)
    \<and> Line_on (Li B3 C3) q \<and> \<not> Bet_Point (Se q C3) B3 \<and> Def (Ang (An p B3 q))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A1 B1 C1))
Def (Ang (An A2 B2 C2))
Def (Ang (An A3 B3 C3))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A1 B1 C1)) add Emp)
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p q. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B3 q)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An p B3 q)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 p)) add Emp) \<and> Line_on (Li B3 A3) p \<and> \<not> Bet_Point (Se p A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 q)) add Emp) \<and> Line_on (Li B3 C3) q \<and> \<not> Bet_Point (Se q C3) B3 \<and> Def (Ang (An p B3 q))
[PROOF STEP]
obtain A31 C31 :: Point where P4 : "Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)
    \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)
    \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp)
    \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3
    \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp)
    \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p q. Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An p B3 q)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An p B3 q)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 p)) add Emp) \<and> Line_on (Li B3 A3) p \<and> \<not> Bet_Point (Se p A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 q)) add Emp) \<and> Line_on (Li B3 C3) q \<and> \<not> Bet_Point (Se q C3) B3 \<and> Def (Ang (An p B3 q))

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
[PROOF STEP]
have P6 : "Def (Tri (Tr B2 A21 C21))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P2 P5 P6
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Def (Tri (Tr B1 A1 C1))
Def (Tri (Tr B2 A21 C21))
[PROOF STEP]
have "Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A21 C21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Def (Tri (Tr B1 A1 C1))
Def (Tri (Tr B2 A21 C21))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A21 C21)) add Emp)
[PROOF STEP]
have P7 : "Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A21 C21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B2 A21 C21)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))
[PROOF STEP]
have P8 : "Def (Tri (Tr B3 A31 C31))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P4 P5 P8
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))
Def (Tri (Tr B1 A1 C1))
Def (Tri (Tr B3 A31 C31))
[PROOF STEP]
have "Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B3 A31 C31)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))
Def (Tri (Tr B1 A1 C1))
Def (Tri (Tr B3 A31 C31))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B3 A31 C31)) add Emp)
[PROOF STEP]
have P9 : "Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr B1 A1 C1)) add Emp) (Geos (Tri (Tr B3 A31 C31)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B2 A21 C21))
[PROOF STEP]
have P10 : "Def (Tri (Tr A21 C21 B2))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B2 A21 C21))

goal (1 subgoal):
 1. Def (Tri (Tr A21 C21 B2))
[PROOF STEP]
by (blast intro:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A21 C21 B2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B3 A31 C31))
[PROOF STEP]
have P11 : "Def (Tri (Tr A31 C31 B3))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B3 A31 C31))

goal (1 subgoal):
 1. Def (Tri (Tr A31 C31 B3))
[PROOF STEP]
by (blast intro:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr A31 C31 B3))

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P7 P9
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A21 C21)) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)
[PROOF STEP]
have P12 : "Eq (Geos (Seg (Se A21 C21)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A21 C21)) add Emp)
Eq (Geos (Seg (Se A1 C1)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A21 C21)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A21 C21)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P2 P4
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))
[PROOF STEP]
have P13 : "Eq (Geos (Seg (Se B2 A21)) add Emp) (Geos (Seg (Se B3 A31)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P2 P4
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))
[PROOF STEP]
have P14 : "Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se B3 C31)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
have P15 : "Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se C21 B2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se C21 B2)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se C21 B2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
have P16 : "Eq (Geos (Seg (Se B3 C31)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B3 C31)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B3 C31)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P14 P15 P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se B3 C31)) add Emp)
Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se C21 B2)) add Emp)
Eq (Geos (Seg (Se B3 C31)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)
[PROOF STEP]
have P17 : "Eq (Geos (Seg (Se C21 B2)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se B3 C31)) add Emp)
Eq (Geos (Seg (Se B2 C21)) add Emp) (Geos (Seg (Se C21 B2)) add Emp)
Eq (Geos (Seg (Se B3 C31)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P10 P11 P12 P13 P17
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A21 C21 B2))
Def (Tri (Tr A31 C31 B3))
Eq (Geos (Seg (Se A21 C21)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)
Eq (Geos (Seg (Se B2 A21)) add Emp) (Geos (Seg (Se B3 A31)) add Emp)
Eq (Geos (Seg (Se C21 B2)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)
[PROOF STEP]
have "Cong (Geos (Tri (Tr A21 C21 B2)) add Emp) (Geos (Tri (Tr A31 C31 B3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A21 C21 B2))
Def (Tri (Tr A31 C31 B3))
Eq (Geos (Seg (Se A21 C21)) add Emp) (Geos (Seg (Se A31 C31)) add Emp)
Eq (Geos (Seg (Se B2 A21)) add Emp) (Geos (Seg (Se B3 A31)) add Emp)
Eq (Geos (Seg (Se C21 B2)) add Emp) (Geos (Seg (Se C31 B3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr A21 C21 B2)) add Emp) (Geos (Tri (Tr A31 C31 B3)) add Emp)
[PROOF STEP]
by (simp add:Tri_SSS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr A21 C21 B2)) add Emp) (Geos (Tri (Tr A31 C31 B3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr A21 C21 B2)) add Emp) (Geos (Tri (Tr A31 C31 B3)) add Emp)
[PROOF STEP]
have P18 : "Cong (Geos (Ang (An A21 B2 C21)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr A21 C21 B2)) add Emp) (Geos (Tri (Tr A31 C31 B3)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A21 B2 C21)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A21 B2 C21)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P2 P18
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Cong (Geos (Ang (An A21 B2 C21)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)
[PROOF STEP]
have P19 : "Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A21 B2 C21)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B2 A21)) add Emp) \<and> Line_on (Li B2 A2) A21 \<and> \<not> Bet_Point (Se A21 A2) B2 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B2 C21)) add Emp) \<and> Line_on (Li B2 C2) C21 \<and> \<not> Bet_Point (Se C21 C2) B2 \<and> Def (Ang (An A21 B2 C21))
Cong (Geos (Ang (An A21 B2 C21)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)
[PROOF STEP]
from P4 P19
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A3 B3 C3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A1 B1 C1)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Ang (An A3 B3 C3)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp) \<and> Eq (Geos (Seg (Se B1 A1)) add Emp) (Geos (Seg (Se B3 A31)) add Emp) \<and> Line_on (Li B3 A3) A31 \<and> \<not> Bet_Point (Se A31 A3) B3 \<and> Eq (Geos (Seg (Se B1 C1)) add Emp) (Geos (Seg (Se B3 C31)) add Emp) \<and> Line_on (Li B3 C3) C31 \<and> \<not> Bet_Point (Se C31 C3) B3 \<and> Def (Ang (An A31 B3 C31))
Cong (Geos (Ang (An A2 B2 C2)) add Emp) (Geos (Ang (An A31 B3 C31)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_move_unique_inv :
  assumes
    "Def (Ang (An p1 p2 p3))" "Def (Ang (An p4 p2 p3))"
    "Plane_sameside (Li p2 p3) p1 p4"
    "Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)"
  shows
    "Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
have P1 : "Line_on (Li p2 p4) p4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p4) p4
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p4) p4

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
Line_on (Li p2 p4) p4
[PROOF STEP]
have P2 : "Line_on (Li p2 p1) p4"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
Line_on (Li p2 p4) p4

goal (1 subgoal):
 1. Line_on (Li p2 p1) p4
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p1) p4

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
have P3 : "Line_on (Li p2 p3) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p3) p2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p2

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
[PROOF STEP]
have P4 : "\<not> Line_on (Li p2 p3) p1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
[PROOF STEP]
have P5 : "\<not> Line_on (Li p2 p3) p4"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from P3 P4 P5
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p3) p2
\<not> Line_on (Li p2 p3) p1
\<not> Line_on (Li p2 p3) p4
[PROOF STEP]
have "Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on (Li p2 p3) p \<and>
    \<not> Line_on (Li p2 p3) p1 \<and> \<not> Line_on (Li p2 p3) p4"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p3) p2
\<not> Line_on (Li p2 p3) p1
\<not> Line_on (Li p2 p3) p4

goal (1 subgoal):
 1. Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on (Li p2 p3) p \<and> \<not> Line_on (Li p2 p3) p1 \<and> \<not> Line_on (Li p2 p3) p4
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on (Li p2 p3) p \<and> \<not> Line_on (Li p2 p3) p1 \<and> \<not> Line_on (Li p2 p3) p4

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on (Li p2 p3) p \<and> \<not> Line_on (Li p2 p3) p1 \<and> \<not> Line_on (Li p2 p3) p4
[PROOF STEP]
have "Bet_Point (Se p1 p4) p2 \<Longrightarrow> Plane_diffside (Li p2 p3) p1 p4"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<exists>p. Bet_Point (Se p1 p4) p \<and> Line_on (Li p2 p3) p \<and> \<not> Line_on (Li p2 p3) p1 \<and> \<not> Line_on (Li p2 p3) p4

goal (1 subgoal):
 1. Bet_Point (Se p1 p4) p2 \<Longrightarrow> Plane_diffside (Li p2 p3) p1 p4
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> Plane_diffside (Li p2 p3) p1 p4

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> Plane_diffside (Li p2 p3) p1 p4
[PROOF STEP]
have P6 : "Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<not> Plane_sameside (Li p2 p3) p1 p4"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> Plane_diffside (Li p2 p3) p1 p4

goal (1 subgoal):
 1. Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<not> Plane_sameside (Li p2 p3) p1 p4
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<not> Plane_sameside (Li p2 p3) p1 p4

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from assms P6
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<not> Plane_sameside (Li p2 p3) p1 p4
[PROOF STEP]
have P7 : "\<not> Bet_Point (Se p1 p4) p2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
Bet_Point (Se p1 p4) p2 \<Longrightarrow> \<not> Plane_sameside (Li p2 p3) p1 p4

goal (1 subgoal):
 1. \<not> Bet_Point (Se p1 p4) p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p1 p4) p2

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
have P8 : "Line_on (Li p2 p3) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p3) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p3

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
have P9 : "\<not> Bet_Point (Se p3 p3) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se p3 p3) p2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p3 p3) p2

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
[PROOF STEP]
have P11 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
from assms P2 P7 P8 P9 P10 P11
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
Line_on (Li p2 p1) p4
\<not> Bet_Point (Se p1 p4) p2
Line_on (Li p2 p3) p3
\<not> Bet_Point (Se p3 p3) p2
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have "Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
    \<and> Def (Ang (An p4 p2 p3))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Def (Ang (An p4 p2 p3))
Plane_sameside (Li p2 p3) p1 p4
Eq (Geos (Lin (Li p2 p1)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
Line_on (Li p2 p1) p4
\<not> Bet_Point (Se p1 p4) p2
Line_on (Li p2 p3) p3
\<not> Bet_Point (Se p3 p3) p2
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
thus "Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp) \<and> Def (Ang (An p4 p2 p3))

goal (1 subgoal):
 1. Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p1 p2 p3)) add Emp) (Geos (Ang (An p4 p2 p3)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed