[STATEMENT]
lemma (in Congruence_Rule) Ang_Gr_trans_Gr_Gr :
  assumes
    "Def (Ang (An p11 p12 p13))" "Def (Ang (An p21 p22 p23))" "Def (Ang (An p31 p32 p33))"
    "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
    "Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
  shows
    "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P1 : "\<not> Line_on (Li p12 p13) p11"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p12 p13) p11
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p12 p13) p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p12 p13) p11
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p p11"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p12 p13) p11

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11
[PROOF STEP]
obtain p14 :: Point where P2 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p14 p11"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

goal (1 subgoal):
 1. (\<And>p14. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p12 p13) p11
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p p11"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Line_on (Li p12 p13) p11

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11
[PROOF STEP]
by (simp add:Ang_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11
[PROOF STEP]
obtain p15 :: Point where P3 : "Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
    \<and> Plane_sameside (Li p12 p13) p15 p11"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p p11

goal (1 subgoal):
 1. (\<And>p15. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p15 p11 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P4 : "Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P5 : "Plane_sameside (Li p12 p13) p14 p11"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p15 p11
[PROOF STEP]
have P6 : "Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p15 p11
[PROOF STEP]
have P7 : "Plane_sameside (Li p12 p13) p15 p11"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. Plane_sameside (Li p12 p13) p15 p11
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P4 P5
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have "Ang_inside (An p11 p12 p13) p14 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p14 p11

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P8 : "Ang_inside (An p11 p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p14
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p14 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p14
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p14

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p14 p11
[PROOF STEP]
have P9 : "\<not> Line_on (Li p12 p13) p14"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p14 p11

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P9 P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p12 p13) p14
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have "Def (Ang (An p12 p13 p14))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p12 p13) p14
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p12 p13 p14))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p12 p13 p14))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p12 p13 p14))
[PROOF STEP]
have P11 : "Def (Ang (An p14 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p12 p13 p14))

goal (1 subgoal):
 1. Def (Ang (An p14 p12 p13))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p14 p12 p13))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P4 P11
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))
[PROOF STEP]
have P12 : "Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Eq_Gr Ang_rev)
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p14 p12 p13))
[PROOF STEP]
have P13 : "Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow>
    Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p14 p12 p13))

goal (1 subgoal):
 1. Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
[PROOF STEP]
by (simp add:Ang_Eq_Point)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
[PROOF STEP]
have P14 : "Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))

goal (1 subgoal):
 1. Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P4 P11 P13 P14
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
[PROOF STEP]
have P15 : "Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p14 p12 p13)) add Emp)
Def (Ang (An p14 p12 p13))
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P6 P13 P15
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
[PROOF STEP]
have P16 : "Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow>
    Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Eq (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P17 : "\<not> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. \<not> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
by (simp add:Ang_Gr_not_Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P16 P17
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
\<not> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
[PROOF STEP]
have P18 : "\<not> Eq (Geos (Poi p15) add Emp) (Geos (Poi p14) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi p14) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
\<not> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p15 p11
[PROOF STEP]
have P19 : "Plane_sameside (Li p12 p13) p11 p15"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. Plane_sameside (Li p12 p13) p11 p15
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p13) p11 p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P5 P18 P19
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p14 p11
\<not> Eq (Geos (Poi p15) add Emp) (Geos (Poi p14) add Emp)
Plane_sameside (Li p12 p13) p11 p15
[PROOF STEP]
have P20 : "Plane_sameside (Li p12 p13) p15 p14"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p14 p11
\<not> Eq (Geos (Poi p15) add Emp) (Geos (Poi p14) add Emp)
Plane_sameside (Li p12 p13) p11 p15

goal (1 subgoal):
 1. Plane_sameside (Li p12 p13) p15 p14
[PROOF STEP]
by (blast intro:Plane_sameside_trans Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p13) p15 p14

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P6 P20
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p15 p14
[PROOF STEP]
have P21 : "Ang_inside (An p14 p12 p13) p15 \<longleftrightarrow>
    Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p15 p14

goal (1 subgoal):
 1. Ang_inside (An p14 p12 p13) p15 = Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p14 p12 p13) p15 = Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P12 P21
[PROOF STATE]
proof (chain)
picking this:
Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Ang_inside (An p14 p12 p13) p15 = Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have "Ang_inside (An p14 p12 p13) p15"
[PROOF STATE]
proof (prove)
using this:
Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Ang_inside (An p14 p12 p13) p15 = Gr (Geos (Ang (An p14 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An p14 p12 p13) p15
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Ang_inside (An p14 p12 p13) p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p14 p12 p13) p15
[PROOF STEP]
have P22 : "Plane_sameside (Li p12 p14) p13 p15 \<and> Plane_sameside (Li p12 p13) p14 p15"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p14 p12 p13) p15

goal (1 subgoal):
 1. Plane_sameside (Li p12 p14) p13 p15 \<and> Plane_sameside (Li p12 p13) p14 p15
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p14) p13 p15 \<and> Plane_sameside (Li p12 p13) p14 p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p11 p12 p13) p14
[PROOF STEP]
have P23 : "Plane_sameside (Li p12 p11) p13 p14 \<and> Plane_sameside (Li p12 p13) p11 p14"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p14

goal (1 subgoal):
 1. Plane_sameside (Li p12 p11) p13 p14 \<and> Plane_sameside (Li p12 p13) p11 p14
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p11) p13 p14 \<and> Plane_sameside (Li p12 p13) p11 p14

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p11) p13 p14 \<and> Plane_sameside (Li p12 p13) p11 p14
[PROOF STEP]
have P24 : "Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> Plane_diffside (Li p12 p11) p14 p15"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p11) p13 p14 \<and> Plane_sameside (Li p12 p13) p11 p14

goal (1 subgoal):
 1. Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> Plane_diffside (Li p12 p11) p14 p15
[PROOF STEP]
by (blast intro:Plane_trans)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> Plane_diffside (Li p12 p11) p14 p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p11 p12 p13) p14
[PROOF STEP]
have P25 : "Plane_diffside (Li p12 p14) p11 p13"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p14

goal (1 subgoal):
 1. Plane_diffside (Li p12 p14) p11 p13
[PROOF STEP]
by (simp add:Ang_inside_Planeside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p12 p14) p11 p13

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P22 P25
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p14) p13 p15 \<and> Plane_sameside (Li p12 p13) p14 p15
Plane_diffside (Li p12 p14) p11 p13
[PROOF STEP]
have P26 : "Plane_diffside (Li p12 p14) p11 p15"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p14) p13 p15 \<and> Plane_sameside (Li p12 p13) p14 p15
Plane_diffside (Li p12 p14) p11 p13

goal (1 subgoal):
 1. Plane_diffside (Li p12 p14) p11 p15
[PROOF STEP]
by (blast intro:Plane_trans Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p12 p14) p11 p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P5 P7 P24 P26
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p14 p11
Plane_sameside (Li p12 p13) p15 p11
Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> Plane_diffside (Li p12 p11) p14 p15
Plane_diffside (Li p12 p14) p11 p15
[PROOF STEP]
have "Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p14 p11
Plane_sameside (Li p12 p13) p15 p11
Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> Plane_diffside (Li p12 p11) p14 p15
Plane_diffside (Li p12 p14) p11 p15

goal (1 subgoal):
 1. Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> False
[PROOF STEP]
by (blast intro:Planeside_wrong_relation)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> False

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> False
[PROOF STEP]
have P27 : "\<not> Plane_diffside (Li p12 p11) p13 p15"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li p12 p11) p13 p15 \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> Plane_diffside (Li p12 p11) p13 p15
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Plane_diffside (Li p12 p11) p13 p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P23
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p11) p13 p14 \<and> Plane_sameside (Li p12 p13) p11 p14
[PROOF STEP]
have P28 : "\<not> Line_on (Li p12 p11) p13"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p11) p13 p14 \<and> Plane_sameside (Li p12 p13) p11 p14

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P29 : "Line_on (Li p12 p13) p12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p12 p13) p12
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p12 p13) p12

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P19
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p11 p15
[PROOF STEP]
have P30 : "\<not> Line_on (Li p12 p13) p11"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p15

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P19
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p11 p15
[PROOF STEP]
have P31 : "\<not> Line_on (Li p12 p13) p15"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p11 p15

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P29 P30 P31
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p12 p13) p12
\<not> Line_on (Li p12 p13) p11
\<not> Line_on (Li p12 p13) p15
[PROOF STEP]
have "Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<exists>p. Bet_Point (Se p11 p15) p \<and>
    Line_on (Li p12 p13) p \<and> \<not> Line_on (Li p12 p13) p11 \<and> \<not> Line_on (Li p12 p13) p15"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p12 p13) p12
\<not> Line_on (Li p12 p13) p11
\<not> Line_on (Li p12 p13) p15

goal (1 subgoal):
 1. Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<exists>p. Bet_Point (Se p11 p15) p \<and> Line_on (Li p12 p13) p \<and> \<not> Line_on (Li p12 p13) p11 \<and> \<not> Line_on (Li p12 p13) p15
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<exists>p. Bet_Point (Se p11 p15) p \<and> Line_on (Li p12 p13) p \<and> \<not> Line_on (Li p12 p13) p11 \<and> \<not> Line_on (Li p12 p13) p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<exists>p. Bet_Point (Se p11 p15) p \<and> Line_on (Li p12 p13) p \<and> \<not> Line_on (Li p12 p13) p11 \<and> \<not> Line_on (Li p12 p13) p15
[PROOF STEP]
have "Bet_Point (Se p11 p15) p12 \<Longrightarrow> Plane_diffside (Li p12 p13) p11 p15"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<exists>p. Bet_Point (Se p11 p15) p \<and> Line_on (Li p12 p13) p \<and> \<not> Line_on (Li p12 p13) p11 \<and> \<not> Line_on (Li p12 p13) p15

goal (1 subgoal):
 1. Bet_Point (Se p11 p15) p12 \<Longrightarrow> Plane_diffside (Li p12 p13) p11 p15
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p11 p15) p12 \<Longrightarrow> Plane_diffside (Li p12 p13) p11 p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p15) p12 \<Longrightarrow> Plane_diffside (Li p12 p13) p11 p15
[PROOF STEP]
have P32 : "Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<not> Plane_sameside (Li p12 p13) p15 p11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p15) p12 \<Longrightarrow> Plane_diffside (Li p12 p13) p11 p15

goal (1 subgoal):
 1. Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<not> Plane_sameside (Li p12 p13) p15 p11
[PROOF STEP]
by (simp add:Plane_diffside_rev Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<not> Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P7 P32
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p12 p13) p15 p11
Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<not> Plane_sameside (Li p12 p13) p15 p11
[PROOF STEP]
have P33 : "\<not> Bet_Point (Se p11 p15) p12"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p12 p13) p15 p11
Bet_Point (Se p11 p15) p12 \<Longrightarrow> \<not> Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. \<not> Bet_Point (Se p11 p15) p12
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p11 p15) p12

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P34 : "Line_on (Li p12 p13) p13"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p12 p13) p13
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p12 p13) p13

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P35 : "\<not> Bet_Point (Se p13 p13) p12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se p13 p13) p12
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p13 p13) p12

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P29
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p12 p13) p12
[PROOF STEP]
have P36 : "Eq (Geos (Poi p12) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow>
    Line_on (Li p12 p13) p15"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p12 p13) p12

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P31 P36
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p12 p13) p15
Eq (Geos (Poi p12) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Line_on (Li p12 p13) p15
[PROOF STEP]
have P37 : "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p15) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p12 p13) p15
Eq (Geos (Poi p12) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Line_on (Li p12 p13) p15

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P38 : "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P33 P34 P35 P37 P38
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Bet_Point (Se p11 p15) p12
Line_on (Li p12 p13) p13
\<not> Bet_Point (Se p13 p13) p12
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p15) add Emp)
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have P39 : "Line_on (Li p12 p11) p15 \<Longrightarrow>
    Eq (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
\<not> Bet_Point (Se p11 p15) p12
Line_on (Li p12 p13) p13
\<not> Bet_Point (Se p13 p13) p12
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p15) add Emp)
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p13) add Emp)

goal (1 subgoal):
 1. Line_on (Li p12 p11) p15 \<Longrightarrow> Eq (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Eq (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Eq (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
[PROOF STEP]
have P40 : "Line_on (Li p12 p11) p15 \<Longrightarrow>
    Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Eq (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))

goal (1 subgoal):
 1. Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P6 P39 P40
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Line_on (Li p12 p11) p15 \<Longrightarrow> Eq (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
[PROOF STEP]
have P41 : "Line_on (Li p12 p11) p15 \<Longrightarrow>
    Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Line_on (Li p12 p11) p15 \<Longrightarrow> Eq (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp) \<and> Def (Ang (An p15 p12 p13))
Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)

goal (1 subgoal):
 1. Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_trans Ang_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P41
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P42 : "Line_on (Li p12 p11) p15 \<Longrightarrow>
    Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Line_on (Li p12 p11) p15 \<Longrightarrow> Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Line_on (Li p12 p11) p15 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq)
[PROOF STATE]
proof (state)
this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
have P43 : "\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
by (simp add:Ang_Gr_not_Eq_rev)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P42 P43
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
[PROOF STEP]
have P44: "\<not> Line_on (Li p12 p11) p15"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p12 p11) p15 \<Longrightarrow> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)
\<not> Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p11 p12 p13)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p12 p11) p15
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p12 p11) p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P34
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p12 p13) p13
[PROOF STEP]
have P45 : "Eq (Geos (Poi p13) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow>
    Line_on (Li p12 p13) p15"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p12 p13) p13

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P31 P45
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p12 p13) p15
Eq (Geos (Poi p13) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Line_on (Li p12 p13) p15
[PROOF STEP]
have P46 : "\<not> Eq (Geos (Poi p13) add Emp) (Geos (Poi p15) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p12 p13) p15
Eq (Geos (Poi p13) add Emp) (Geos (Poi p15) add Emp) \<Longrightarrow> Line_on (Li p12 p13) p15

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

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P27 P28 P44 P46
[PROOF STATE]
proof (chain)
picking this:
\<not> Plane_diffside (Li p12 p11) p13 p15
\<not> Line_on (Li p12 p11) p13
\<not> Line_on (Li p12 p11) p15
\<not> Eq (Geos (Poi p13) add Emp) (Geos (Poi p15) add Emp)
[PROOF STEP]
have P47 : "Plane_sameside (Li p12 p11) p13 p15"
[PROOF STATE]
proof (prove)
using this:
\<not> Plane_diffside (Li p12 p11) p13 p15
\<not> Line_on (Li p12 p11) p13
\<not> Line_on (Li p12 p11) p15
\<not> Eq (Geos (Poi p13) add Emp) (Geos (Poi p15) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li p12 p11) p13 p15
[PROOF STEP]
by (simp add:Plane_not_diffside_sameside)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p12 p11) p13 p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from assms P19 P47
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Plane_sameside (Li p12 p13) p11 p15
Plane_sameside (Li p12 p11) p13 p15
[PROOF STEP]
have P48 : "Ang_inside (An p11 p12 p13) p15"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p11 p12 p13))
Def (Ang (An p21 p22 p23))
Def (Ang (An p31 p32 p33))
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p21 p22 p23)) add Emp)
Gr (Geos (Ang (An p21 p22 p23)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
Plane_sameside (Li p12 p13) p11 p15
Plane_sameside (Li p12 p11) p13 p15

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p15
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p15

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P6 P7
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p15 p11
[PROOF STEP]
have P49 : "Ang_inside (An p11 p12 p13) p15 \<longleftrightarrow>
    Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An p31 p32 p33)) add Emp) (Geos (Ang (An p15 p12 p13)) add Emp)
Plane_sameside (Li p12 p13) p15 p11

goal (1 subgoal):
 1. Ang_inside (An p11 p12 p13) p15 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
by (simp add:Ang_greater_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p11 p12 p13) p15 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
from P48 P49
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An p11 p12 p13) p15
Ang_inside (An p11 p12 p13) p15 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
show "Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An p11 p12 p13) p15
Ang_inside (An p11 p12 p13) p15 = Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal (1 subgoal):
 1. Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Gr (Geos (Ang (An p11 p12 p13)) add Emp) (Geos (Ang (An p31 p32 p33)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed