[STATEMENT]
theorem (in Congruence_Rule) Tri_week_SSS :
  assumes
    "Plane_diffside (Li x y) z1 z2"
    "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)"
    "Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)"
    "Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)"
  shows "Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
[PROOF STEP]
have "\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p
    \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
[PROOF STEP]
obtain pn :: Point where P1 : "Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn
    \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. (\<And>pn. Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P2 : "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P2
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
[PROOF STEP]
have "\<not> (Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp))"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp))
[PROOF STEP]
have P3 : "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp)
    \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp)
    \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> (Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp))

goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
[PROOF STEP]
have P4 : "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P4
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
have P5 : "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li x y) p \<and> Eq (Geos (Poi x) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_SSS_lemma1)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li x y) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li x y) x
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li x y) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li x y) x
[PROOF STEP]
have P7 : "Eq (Geos (Poi x) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li x y) x

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P7
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi x) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P8 : "\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi x) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi x) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P9 : "Line_on (Li x y) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li x y) y
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li x y) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li x y) y
[PROOF STEP]
have P10 : "Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li x y) y

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P10
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P11 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp) \<Longrightarrow> Line_on (Li x y) z1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
[PROOF STEP]
have "Def (Tri (Tr x y z1))"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. Def (Tri (Tr x y z1))
[PROOF STEP]
by (simp add:Ang_sinple_def Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr x y z1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr x y z1))
[PROOF STEP]
have P12 : "Def (Tri (Tr z1 x y))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr x y z1))

goal (1 subgoal):
 1. Def (Tri (Tr z1 x y))
[PROOF STEP]
by (simp add:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr z1 x y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li x y) x
[PROOF STEP]
have P13 : "Eq (Geos (Poi x) add Emp) (Geos (Poi z2) add Emp) \<Longrightarrow> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li x y) x

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P13
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi x) add Emp) (Geos (Poi z2) add Emp) \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
have P14 : "\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi x) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi x) add Emp) (Geos (Poi z2) add Emp) \<Longrightarrow> Line_on (Li x y) z2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li x y) y
[PROOF STEP]
have P15 : "Eq (Geos (Poi y) add Emp) (Geos (Poi z2) add Emp) \<Longrightarrow> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li x y) y

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P15
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi y) add Emp) (Geos (Poi z2) add Emp) \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
have P16 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Poi y) add Emp) (Geos (Poi z2) add Emp) \<Longrightarrow> Line_on (Li x y) z2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
[PROOF STEP]
have "Def (Tri (Tr x y z2))"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. Def (Tri (Tr x y z2))
[PROOF STEP]
by (simp add:Ang_sinple_def Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr x y z2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr x y z2))
[PROOF STEP]
have P17 : "Def (Tri (Tr z2 x y))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr x y z2))

goal (1 subgoal):
 1. Def (Tri (Tr z2 x y))
[PROOF STEP]
by (simp add:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr z2 x y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P18 : "Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se z1 x)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se z1 x)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se z1 x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P19 : "Eq (Geos (Seg (Se x z2)) add Emp) (Geos (Seg (Se z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se x z2)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se x z2)) add Emp) (Geos (Seg (Se z2 x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P18
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se z1 x)) add Emp)
[PROOF STEP]
have P20 : "Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se x z2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se z1 x)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P19 P20
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se x z2)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se x z2)) add Emp)
[PROOF STEP]
have P21 : "Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se x z2)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se x z2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P22 : "Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se z1 y)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se z1 y)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se z1 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P23 : "Eq (Geos (Seg (Se y z2)) add Emp) (Geos (Seg (Se z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se y z2)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se y z2)) add Emp) (Geos (Seg (Se z2 y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P22
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se z1 y)) add Emp)
[PROOF STEP]
have P24 : "Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se y z2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se z1 y)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P23 P24
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se y z2)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se y z2)) add Emp)
[PROOF STEP]
have P25 : "Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se z2 y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se y z2)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se y z2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P5 P12 P17 P21 P25
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
Def (Tri (Tr z1 x y))
Def (Tri (Tr z2 x y))
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
[PROOF STEP]
have "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Tri (Tr z1 x y)) add Emp) (Geos (Tri (Tr z2 x y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 y)) add Emp) (Geos (Ang (An x z2 y)) add Emp)
Def (Tri (Tr z1 x y))
Def (Tri (Tr z2 x y))
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se z2 y)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 x y)) add Emp) (Geos (Tri (Tr z2 x y)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 x y)) add Emp) (Geos (Tri (Tr z2 x y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 x y)) add Emp) (Geos (Tri (Tr z2 x y)) add Emp)
[PROOF STEP]
have P26 : "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An z2 y x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 x y)) add Emp) (Geos (Tri (Tr z2 x y)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An z2 y x)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An z2 y x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P27 : "Eq (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An x y z1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An x y z1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An x y z1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P28 : "Eq (Geos (Ang (An z2 y x)) add Emp) (Geos (Ang (An x y z2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An z2 y x)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An z2 y x)) add Emp) (Geos (Ang (An x y z2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P26 P27
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An z2 y x)) add Emp)
Eq (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An x y z1)) add Emp)
[PROOF STEP]
have P29 : "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An z2 y x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An z2 y x)) add Emp)
Eq (Geos (Ang (An z1 y x)) add Emp) (Geos (Ang (An x y z1)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An z2 y x)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An z2 y x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P28 P29
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An z2 y x)) add Emp) (Geos (Ang (An x y z2)) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An z2 y x)) add Emp)
[PROOF STEP]
have P30 : "Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An z2 y x)) add Emp) (Geos (Ang (An x y z2)) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An z2 y x)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
[PROOF STEP]
have P31 : "Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li y x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P31
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li y x)) add Emp)
[PROOF STEP]
have P32 : "Plane_diffside (Li y x) z1 z2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li y x)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li y x) z1 z2
[PROOF STEP]
by (simp add:Plane_Line_diff_trans)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li y x) z1 z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
[PROOF STEP]
have P33 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi x) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P31
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li y x)) add Emp)
[PROOF STEP]
have P34 : "Line_on (Li y x) pn"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li y x)) add Emp)

goal (1 subgoal):
 1. Line_on (Li y x) pn
[PROOF STEP]
by (blast intro:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li y x) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P34
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li y x) pn
[PROOF STEP]
have P35 : "Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li y x) p \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li y x) pn

goal (1 subgoal):
 1. Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li y x) p \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li y x) p \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P32 P33 P35
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Plane_diffside (Li y x) z1 z2
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi x) add Emp)
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li y x) p \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
have P36 : "Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Plane_diffside (Li y x) z1 z2
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi x) add Emp)
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<exists>p. Bet_Point (Se z1 z2) p \<and> Line_on (Li y x) p \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
[PROOF STEP]
by (simp add:Tri_week_SSS_lemma1)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr z1 x y))
[PROOF STEP]
have P37 : "Def (Tri (Tr z1 y x))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr z1 x y))

goal (1 subgoal):
 1. Def (Tri (Tr z1 y x))
[PROOF STEP]
by (blast intro:Tri_def_trans Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr z1 y x))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P17
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr z2 x y))
[PROOF STEP]
have P38 : "Def (Tri (Tr z2 y x))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr z2 x y))

goal (1 subgoal):
 1. Def (Tri (Tr z2 y x))
[PROOF STEP]
by (blast intro:Tri_def_trans Tri_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr z2 y x))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P21 P25 P36 P37 P38
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
Def (Tri (Tr z1 y x))
Def (Tri (Tr z2 y x))
[PROOF STEP]
have "Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
Def (Tri (Tr z1 y x))
Def (Tri (Tr z2 y x))

goal (1 subgoal):
 1. Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)
[PROOF STEP]
have P39 : "Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
[PROOF STEP]
have P40 : "Bet_Point (Se z1 z2) pn"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2

goal (1 subgoal):
 1. Bet_Point (Se z1 z2) pn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se z1 z2) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P41 : "Line_on (Li z1 z2) pn"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

goal (1 subgoal):
 1. Line_on (Li z1 z2) pn
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have "Line_on (Li z1 z2) z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z1 z2) z1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 z2) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z1 z2) z1
[PROOF STEP]
have P42 : "Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp) \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z1 z2) z1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp) \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P42
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P43 : "\<not> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp) \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P6 P41
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li x y) x
Line_on (Li z1 z2) pn
[PROOF STEP]
have P44 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Line_on (Li z1 z2) x \<Longrightarrow>
    Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li x y) x
Line_on (Li z1 z2) pn

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) x\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) x\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P43 P44
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) x\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
have P45 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    \<not> Line_on (Li z1 z2) x"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) x\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P46 : "\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P45 P46
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) x
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Tri (Tr z1 z2 x))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) x
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 x))
[PROOF STEP]
by (simp add:Ang_sinple_def Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 x))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 x))
[PROOF STEP]
have P47 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Tri (Tr x z1 z2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 x))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))
[PROOF STEP]
by (simp add:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P47
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))
[PROOF STEP]
have P48 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)
[PROOF STEP]
by (simp add:Tri_isosceles)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P49 : "Line_on (Li z1 x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z1 x) x
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 x) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P50 : "\<not> Bet_Point (Se x x) z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se x x) z1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se x x) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P51 : "Inv (Bet_Point (Se z2 pn) z1) \<and> Inv (Bet_Point (Se pn z1) z2)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

goal (1 subgoal):
 1. Inv (Bet_Point (Se z2 pn) z1) \<and> Inv (Bet_Point (Se pn z1) z2)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se z2 pn) z1) \<and> Inv (Bet_Point (Se pn z1) z2)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se z2 pn) z1) \<and> Inv (Bet_Point (Se pn z1) z2)
[PROOF STEP]
have P52 : "\<not> Bet_Point (Se z2 pn) z1"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se z2 pn) z1) \<and> Inv (Bet_Point (Se pn z1) z2)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have "\<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi z1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi z1) add Emp)
[PROOF STEP]
have P53 : "\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi z1) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P47
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))
[PROOF STEP]
have P54 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Ang (An x z1 z2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z1 z2))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z1 z2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P8 P41 P49 P50 P52 P53 P54
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi x) add Emp)
Line_on (Li z1 z2) pn
Line_on (Li z1 x) x
\<not> Bet_Point (Se x x) z1
\<not> Bet_Point (Se z2 pn) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z1 z2))
[PROOF STEP]
have P55 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z1 pn)) add Emp) \<and> Def (Ang (An x z1 pn))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi x) add Emp)
Line_on (Li z1 z2) pn
Line_on (Li z1 x) x
\<not> Bet_Point (Se x x) z1
\<not> Bet_Point (Se z2 pn) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z1 z2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z1 pn)) add Emp) \<and> Def (Ang (An x z1 pn))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z1 pn)) add Emp) \<and> Def (Ang (An x z1 pn))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P48 P55
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z1 pn)) add Emp) \<and> Def (Ang (An x z1 pn))
[PROOF STEP]
have P56 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z1 z2)) add Emp) (Geos (Ang (An x z1 pn)) add Emp) \<and> Def (Ang (An x z1 pn))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P47
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))
[PROOF STEP]
have P57 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Ang (An x z2 z1))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr x z1 z2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z2 z1))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z2 z1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P58 : "Line_on (Li z2 x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z2 x) x
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z2 x) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P59 : "\<not> Bet_Point (Se x x) z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se x x) z2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se x x) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P60 : "Line_on (Li z2 z1) pn"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

goal (1 subgoal):
 1. Line_on (Li z2 z1) pn
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li z2 z1) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P51
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se z2 pn) z1) \<and> Inv (Bet_Point (Se pn z1) z2)
[PROOF STEP]
have "\<not> Bet_Point (Se pn z1) z2"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se z2 pn) z1) \<and> Inv (Bet_Point (Se pn z1) z2)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se pn z1) z2
[PROOF STEP]
have P61 : "\<not> Bet_Point (Se z1 pn) z2"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se pn z1) z2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn
[PROOF STEP]
have P62 : "\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P14 P57 P58 P59 P60 P61 P62
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi x) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z2 z1))
Line_on (Li z2 x) x
\<not> Bet_Point (Se x x) z2
Line_on (Li z2 z1) pn
\<not> Bet_Point (Se z1 pn) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
[PROOF STEP]
have P63 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An x z2 z1)) add Emp) (Geos (Ang (An x z2 pn)) add Emp) \<and> Def (Ang (An x z2 pn))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi x) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An x z2 z1))
Line_on (Li z2 x) x
\<not> Bet_Point (Se x x) z2
Line_on (Li z2 z1) pn
\<not> Bet_Point (Se z1 pn) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z2 z1)) add Emp) (Geos (Ang (An x z2 pn)) add Emp) \<and> Def (Ang (An x z2 pn))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z2 z1)) add Emp) (Geos (Ang (An x z2 pn)) add Emp) \<and> Def (Ang (An x z2 pn))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P56 P63
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z2 z1)) add Emp) (Geos (Ang (An x z2 pn)) add Emp) \<and> Def (Ang (An x z2 pn))
[PROOF STEP]
have P64 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 z1)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An x z2 z1)) add Emp) (Geos (Ang (An x z2 pn)) add Emp) \<and> Def (Ang (An x z2 pn))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P9 P41
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li x y) y
Line_on (Li z1 z2) pn
[PROOF STEP]
have P65 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Line_on (Li z1 z2) y \<Longrightarrow>
    Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li x y) y
Line_on (Li z1 z2) pn

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) y\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) y\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P43 P65
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) y\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
have P66 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    \<not> Line_on (Li z1 z2) y"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Line_on (Li z1 z2) y\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li z1 z2)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P46 P66
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) y
[PROOF STEP]
have "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Tri (Tr z1 z2 y))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi z2) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Line_on (Li z1 z2) y

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 y))
[PROOF STEP]
by (simp add:Ang_sinple_def Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 y))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 y))
[PROOF STEP]
have P67 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Tri (Tr y z1 z2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr z1 z2 y))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr y z1 z2))
[PROOF STEP]
by (simp add:Tri_def_trans)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr y z1 z2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P67
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr y z1 z2))
[PROOF STEP]
have P68 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr y z1 z2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
[PROOF STEP]
by (simp add:Tri_isosceles)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P67
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr y z1 z2))
[PROOF STEP]
have P69 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Ang (An y z1 z2))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Tri (Tr y z1 z2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z1 z2))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z1 z2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P70 : "Line_on (Li z1 y) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z1 y) y
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 y) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P71 : "\<not> Bet_Point (Se y y) z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se y y) z1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se y y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp)
[PROOF STEP]
have P72 : "\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi y) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z1) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P41 P52 P53 P69 P70 P71 P72
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z1 z2) pn
\<not> Bet_Point (Se z2 pn) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z1 z2))
Line_on (Li z1 y) y
\<not> Bet_Point (Se y y) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi y) add Emp)
[PROOF STEP]
have P73 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z1 pn)) add Emp) \<and> Def (Ang (An y z1 pn))"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z1 z2) pn
\<not> Bet_Point (Se z2 pn) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z1 z2))
Line_on (Li z1 y) y
\<not> Bet_Point (Se y y) z1
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi y) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z1 pn)) add Emp) \<and> Def (Ang (An y z1 pn))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z1 pn)) add Emp) \<and> Def (Ang (An y z1 pn))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P68 P73
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z1 pn)) add Emp) \<and> Def (Ang (An y z1 pn))
[PROOF STEP]
have P74 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z1 z2)) add Emp) (Geos (Ang (An y z1 pn)) add Emp) \<and> Def (Ang (An y z1 pn))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P69
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z1 z2))
[PROOF STEP]
have P75 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Def (Ang (An y z2 z1))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z1 z2))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z2 z1))
[PROOF STEP]
by (simp add:Ang_def_inv)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z2 z1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P76 : "Line_on (Li z2 y) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z2 y) y
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z2 y) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P77 : "\<not> Bet_Point (Se y y) z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se y y) z2
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se y y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z2) add Emp)
[PROOF STEP]
have P78 : "\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi z2) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P60 P61 P62 P75 P76 P77 P78
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z2 z1) pn
\<not> Bet_Point (Se z1 pn) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z2 z1))
Line_on (Li z2 y) y
\<not> Bet_Point (Se y y) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp)
[PROOF STEP]
have P79 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An y z2 pn)) add Emp) \<and> Def (Ang (An y z2 pn))"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z2 z1) pn
\<not> Bet_Point (Se z1 pn) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Def (Ang (An y z2 z1))
Line_on (Li z2 y) y
\<not> Bet_Point (Se y y) z2
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi y) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An y z2 pn)) add Emp) \<and> Def (Ang (An y z2 pn))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An y z2 pn)) add Emp) \<and> Def (Ang (An y z2 pn))

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P74 P79
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An y z2 pn)) add Emp) \<and> Def (Ang (An y z2 pn))
[PROOF STEP]
have P80 : "\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 z1)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Eq (Geos (Ang (An y z2 z1)) add Emp) (Geos (Ang (An y z2 pn)) add Emp) \<and> Def (Ang (An y z2 pn))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P81 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi x) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi x) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi x) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P1 P6 P9 P81
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li x y) x
Line_on (Li x y) y
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi x) add Emp)
[PROOF STEP]
have
    "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Bet_Point (Se x pn) y \<or> Bet_Point (Se pn y) x \<or> Bet_Point (Se y x) pn"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Line_on (Li x y) x
Line_on (Li x y) y
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi pn) add Emp) (Geos (Poi x) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<or> Bet_Point (Se pn y) x \<or> Bet_Point (Se y x) pn
[PROOF STEP]
by (simp add:Bet_case)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<or> Bet_Point (Se pn y) x \<or> Bet_Point (Se y x) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<or> Bet_Point (Se pn y) x \<or> Bet_Point (Se y x) pn
[PROOF STEP]
have P82 :
    "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn
    \<or> \<not> Bet_Point (Se x pn) y \<and> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn
    \<or> \<not> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> Bet_Point (Se y x) pn"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<or> Bet_Point (Se pn y) x \<or> Bet_Point (Se y x) pn

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> Bet_Point (Se y x) pn
[PROOF STEP]
by (simp add:Bet_case_fact)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> Bet_Point (Se y x) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P83 : "Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P84 : "Line_on (Li z1 pn) pn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z1 pn) pn
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 pn) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P85 : "Line_on (Li pn x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li pn x) x
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li pn x) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P83
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y
[PROOF STEP]
have P86 : "Bet_Point (Se x pn) y \<Longrightarrow> Line_on (Li pn x) y"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y

goal (1 subgoal):
 1. Bet_Point (Se x pn) y \<Longrightarrow> Line_on (Li pn x) y
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se x pn) y \<Longrightarrow> Line_on (Li pn x) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P6 P9 P85 P86
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Line_on (Li x y) x
Line_on (Li x y) y
Line_on (Li pn x) x
Bet_Point (Se x pn) y \<Longrightarrow> Line_on (Li pn x) y
[PROOF STEP]
have P87 : "Bet_Point (Se x pn) y \<Longrightarrow>
    Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li x y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Line_on (Li x y) x
Line_on (Li x y) y
Line_on (Li pn x) x
Bet_Point (Se x pn) y \<Longrightarrow> Line_on (Li pn x) y

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P88 : "Line_on (Li z1 pn) z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z1 pn) z1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z1 pn) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P87 P88
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se x pn) y \<Longrightarrow> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li x y)) add Emp)
Line_on (Li z1 pn) z1
[PROOF STEP]
have P89 : "Bet_Point (Se x pn) y \<Longrightarrow>
    Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se x pn) y \<Longrightarrow> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li x y)) add Emp)
Line_on (Li z1 pn) z1

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P89
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P90 : "Bet_Point (Se x pn) y \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P83 P84 P90
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y
Line_on (Li z1 pn) pn
Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)
[PROOF STEP]
have P91 : "Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z1 pn) y x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y
Line_on (Li z1 pn) pn
Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z1 pn) y x
[PROOF STEP]
by (simp add:Plane_Bet_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z1 pn) y x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P92 : "Line_on (Li z2 pn) pn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z2 pn) pn
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z2 pn) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P93 : "Line_on (Li z2 pn) z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li z2 pn) z2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li z2 pn) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P87 P93
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se x pn) y \<Longrightarrow> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li x y)) add Emp)
Line_on (Li z2 pn) z2
[PROOF STEP]
have P94 : "Bet_Point (Se x pn) y \<Longrightarrow>
    Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se x pn) y \<Longrightarrow> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li x y)) add Emp)
Line_on (Li z2 pn) z2

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P94
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
have P95 : "Bet_Point (Se x pn) y \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se x pn) y; Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2

goal (1 subgoal):
 1. Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P83 P92 P95
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y
Line_on (Li z2 pn) pn
Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)
[PROOF STEP]
have P96 : "Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z2 pn) y x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se x pn) y \<Longrightarrow> Bet_Point (Se pn x) y
Line_on (Li z2 pn) pn
Bet_Point (Se x pn) y \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn x)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z2 pn) y x
[PROOF STEP]
by (simp add:Plane_Bet_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z2 pn) y x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P37
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr z1 y x))
[PROOF STEP]
have "Def (Ang (An y z1 x))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr z1 y x))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An y z1 x))
[PROOF STEP]
have P97 : "\<not> Eq (Geos (Lin (Li z1 y)) add Emp) (Geos (Lin (Li z1 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An y z1 x))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P38
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr z2 y x))
[PROOF STEP]
have "Def (Ang (An y z2 x))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr z2 y x))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An y z2 x))
[PROOF STEP]
have P98 : "\<not> Eq (Geos (Lin (Li z2 y)) add Emp) (Geos (Lin (Li z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An y z2 x))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P53 P62 P64 P80 P91 P96 P97 P98
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)
Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z1 pn) y x
Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z2 pn) y x
\<not> Eq (Geos (Lin (Li z1 y)) add Emp) (Geos (Lin (Li z1 x)) add Emp)
\<not> Eq (Geos (Lin (Li z2 y)) add Emp) (Geos (Lin (Li z2 x)) add Emp)
[PROOF STEP]
have P99 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)
    \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<Longrightarrow>
    Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)
Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z1 pn) y x
Bet_Point (Se x pn) y \<Longrightarrow> Plane_sameside (Li z2 pn) y x
\<not> Eq (Geos (Lin (Li z1 y)) add Emp) (Geos (Lin (Li z1 x)) add Emp)
\<not> Eq (Geos (Lin (Li z2 y)) add Emp) (Geos (Lin (Li z2 x)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se x pn) y\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
[PROOF STEP]
by (simp add:Ang_sub)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se x pn) y\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P100 : "Line_on (Li pn y) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li pn y) y
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li pn y) y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P85
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li pn x) x
[PROOF STEP]
have P101 : "Bet_Point (Se pn y) x \<Longrightarrow> Line_on (Li pn y) x"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li pn x) x

goal (1 subgoal):
 1. Bet_Point (Se pn y) x \<Longrightarrow> Line_on (Li pn y) x
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn y) x \<Longrightarrow> Line_on (Li pn y) x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from assms P6 P9 P100 P101
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Line_on (Li x y) x
Line_on (Li x y) y
Line_on (Li pn y) y
Bet_Point (Se pn y) x \<Longrightarrow> Line_on (Li pn y) x
[PROOF STEP]
have P102 : "Bet_Point (Se pn y) x \<Longrightarrow>
    Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li x y)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li x y) z1 z2
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi y) add Emp)
Eq (Geos (Seg (Se x z1)) add Emp) (Geos (Seg (Se x z2)) add Emp)
Eq (Geos (Seg (Se y z1)) add Emp) (Geos (Seg (Se y z2)) add Emp)
Line_on (Li x y) x
Line_on (Li x y) y
Line_on (Li pn y) y
Bet_Point (Se pn y) x \<Longrightarrow> Line_on (Li pn y) x

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P88 P102
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z1 pn) z1
Bet_Point (Se pn y) x \<Longrightarrow> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
have P103 : "Bet_Point (Se pn y) x \<Longrightarrow>
    Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z1 pn) z1
Bet_Point (Se pn y) x \<Longrightarrow> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P103
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P104 : "Bet_Point (Se pn y) x \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P84 P104
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z1 pn) pn
Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)
[PROOF STEP]
have "Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) x y"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z1 pn) pn
Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) x y
[PROOF STEP]
by (simp add:Plane_Bet_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) x y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) x y
[PROOF STEP]
have P105 : "Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) y x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) x y

goal (1 subgoal):
 1. Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) y x
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) y x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P93 P102
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z2 pn) z2
Bet_Point (Se pn y) x \<Longrightarrow> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li x y)) add Emp)
[PROOF STEP]
have P106 : "Bet_Point (Se pn y) x \<Longrightarrow>
    Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z2 pn) z2
Bet_Point (Se pn y) x \<Longrightarrow> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li x y)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P106
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
have P107 : "Bet_Point (Se pn y) x \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
\<lbrakk>Bet_Point (Se pn y) x; Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li x y) z2

goal (1 subgoal):
 1. Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P92 P107
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z2 pn) pn
Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)
[PROOF STEP]
have "Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) x y"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z2 pn) pn
Bet_Point (Se pn y) x \<Longrightarrow> \<not> Eq (Geos (Lin (Li pn y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) x y
[PROOF STEP]
by (simp add:Plane_Bet_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) x y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) x y
[PROOF STEP]
have P108 : "Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) y x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) x y

goal (1 subgoal):
 1. Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) y x
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) y x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P53 P62 P64 P80 P97 P98 P105 P108
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)
\<not> Eq (Geos (Lin (Li z1 y)) add Emp) (Geos (Lin (Li z1 x)) add Emp)
\<not> Eq (Geos (Lin (Li z2 y)) add Emp) (Geos (Lin (Li z2 x)) add Emp)
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) y x
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) y x
[PROOF STEP]
have P109 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)
    \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se pn y) x \<Longrightarrow>
    Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)
\<not> Eq (Geos (Lin (Li z1 y)) add Emp) (Geos (Lin (Li z1 x)) add Emp)
\<not> Eq (Geos (Lin (Li z2 y)) add Emp) (Geos (Lin (Li z2 x)) add Emp)
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z1 pn) y x
Bet_Point (Se pn y) x \<Longrightarrow> Plane_sameside (Li z2 pn) y x

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se pn y) x\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
[PROOF STEP]
by (simp add:Ang_sub)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se pn y) x\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
have P110 : "Bet_Point (Se y x) pn \<Longrightarrow> Bet_Point (Se x y) pn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se y x) pn \<Longrightarrow> Bet_Point (Se x y) pn
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se y x) pn \<Longrightarrow> Bet_Point (Se x y) pn

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P88
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z1 pn) z1
[PROOF STEP]
have P111 : "Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)
    \<Longrightarrow> Line_on (Li x y) z1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z1 pn) z1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P111
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z1
[PROOF STEP]
have P112 : "\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z1

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P84 P110 P112
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z1 pn) pn
Bet_Point (Se y x) pn \<Longrightarrow> Bet_Point (Se x y) pn
\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)
[PROOF STEP]
have "Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) x y"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z1 pn) pn
Bet_Point (Se y x) pn \<Longrightarrow> Bet_Point (Se x y) pn
\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z1 pn)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) x y
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) x y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) x y
[PROOF STEP]
have P113 : "Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) y x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) x y

goal (1 subgoal):
 1. Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) y x
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) y x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P93
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z2 pn) z2
[PROOF STEP]
have P114 : "Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)
    \<Longrightarrow> Line_on (Li x y) z2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z2 pn) z2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z2

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P1 P114
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z2
[PROOF STEP]
have P115 : "\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se z1 z2) pn \<and> Line_on (Li x y) pn \<and> \<not> Line_on (Li x y) z1 \<and> \<not> Line_on (Li x y) z2
Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp) \<Longrightarrow> Line_on (Li x y) z2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P92 P110 P115
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li z2 pn) pn
Bet_Point (Se y x) pn \<Longrightarrow> Bet_Point (Se x y) pn
\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)
[PROOF STEP]
have "Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) x y"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li z2 pn) pn
Bet_Point (Se y x) pn \<Longrightarrow> Bet_Point (Se x y) pn
\<not> Eq (Geos (Lin (Li x y)) add Emp) (Geos (Lin (Li z2 pn)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) x y
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) x y

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) x y
[PROOF STEP]
have P116 : "Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) y x"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) x y

goal (1 subgoal):
 1. Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) y x
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) y x

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P53 P62 P64 P80 P97 P98 P113 P116
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)
\<not> Eq (Geos (Lin (Li z1 y)) add Emp) (Geos (Lin (Li z1 x)) add Emp)
\<not> Eq (Geos (Lin (Li z2 y)) add Emp) (Geos (Lin (Li z2 x)) add Emp)
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) y x
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) y x
[PROOF STEP]
have P117 : "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp)
    \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se y x) pn \<Longrightarrow>
    Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi z1) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi z2) add Emp) (Geos (Poi pn) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x z1 pn)) add Emp) (Geos (Ang (An x z2 pn)) add Emp)
\<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 pn)) add Emp) (Geos (Ang (An y z2 pn)) add Emp)
\<not> Eq (Geos (Lin (Li z1 y)) add Emp) (Geos (Lin (Li z1 x)) add Emp)
\<not> Eq (Geos (Lin (Li z2 y)) add Emp) (Geos (Lin (Li z2 x)) add Emp)
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z1 pn) y x
Bet_Point (Se y x) pn \<Longrightarrow> Plane_diffside (Li z2 pn) y x

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se y x) pn\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
[PROOF STEP]
by (simp add:Ang_add)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se y x) pn\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P82 P99 P109 P117
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> Bet_Point (Se y x) pn
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se x pn) y\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se pn y) x\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se y x) pn\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
[PROOF STEP]
have P118 :
    "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> Bet_Point (Se pn y) x \<and> \<not> Bet_Point (Se y x) pn \<or> \<not> Bet_Point (Se x pn) y \<and> \<not> Bet_Point (Se pn y) x \<and> Bet_Point (Se y x) pn
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se x pn) y\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se pn y) x\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp); Bet_Point (Se y x) pn\<rbrakk> \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P21 P25 P37 P38 P118
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
Def (Tri (Tr z1 y x))
Def (Tri (Tr z2 y x))
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)
[PROOF STEP]
have
    "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se z1 x)) add Emp) (Geos (Seg (Se z2 x)) add Emp)
Eq (Geos (Seg (Se z1 y)) add Emp) (Geos (Seg (Se z2 y)) add Emp)
Def (Tri (Tr z1 y x))
Def (Tri (Tr z2 y x))
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An y z1 x)) add Emp) (Geos (Ang (An y z2 x)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)
[PROOF STEP]
have P119 :
    "\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Tri (Tr z1 y x)) add Emp) (Geos (Tri (Tr z2 y x)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
from P3 P30 P39 P119
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<or> \<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp)
Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
\<not> Eq (Geos (Poi x) add Emp) (Geos (Poi pn) add Emp) \<and> \<not> Eq (Geos (Poi y) add Emp) (Geos (Poi pn) add Emp) \<Longrightarrow> Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An x y z1)) add Emp) (Geos (Ang (An x y z2)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed