[STATEMENT]
theorem (in Congruence_Rule) Ang_sub :
  assumes
    "Plane_sameside (Li o1 l1) h1 k1"
    "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)"
    "Plane_sameside (Li o2 l2) h2 k2"
    "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)"
    "Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)"
    "Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)"
    "\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)"
    "\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)"
  shows
    "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P1 : "\<not> Line_on (Li o1 l1) h1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
\<not> Line_on (Li o1 l1) h1
[PROOF STEP]
have "Def (Ang (An o1 l1 h1))"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
\<not> Line_on (Li o1 l1) h1

goal (1 subgoal):
 1. Def (Ang (An o1 l1 h1))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o1 l1 h1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 l1 h1))
[PROOF STEP]
have P2 : "Def (Ang (An h1 o1 l1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 l1 h1))

goal (1 subgoal):
 1. Def (Ang (An h1 o1 l1))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An h1 o1 l1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P3 : "\<not> Line_on (Li o1 l1) k1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P3
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
\<not> Line_on (Li o1 l1) k1
[PROOF STEP]
have "Def (Ang (An o1 l1 k1))"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
\<not> Line_on (Li o1 l1) k1

goal (1 subgoal):
 1. Def (Ang (An o1 l1 k1))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o1 l1 k1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 l1 k1))
[PROOF STEP]
have P4 : "Def (Ang (An k1 o1 l1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 l1 k1))

goal (1 subgoal):
 1. Def (Ang (An k1 o1 l1))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An k1 o1 l1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P2 P4
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Def (Ang (An h1 o1 l1))
Def (Ang (An k1 o1 l1))
[PROOF STEP]
have P5 : "Ang_inside (An h1 o1 l1) k1 \<and> \<not> Ang_inside (An k1 o1 l1) h1
    \<or> \<not> Ang_inside (An h1 o1 l1) k1 \<and> Ang_inside (An k1 o1 l1) h1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Def (Ang (An h1 o1 l1))
Def (Ang (An k1 o1 l1))

goal (1 subgoal):
 1. Ang_inside (An h1 o1 l1) k1 \<and> \<not> Ang_inside (An k1 o1 l1) h1 \<or> \<not> Ang_inside (An h1 o1 l1) k1 \<and> Ang_inside (An k1 o1 l1) h1
[PROOF STEP]
by (simp add:Ang_inside_case)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 l1) k1 \<and> \<not> Ang_inside (An k1 o1 l1) h1 \<or> \<not> Ang_inside (An h1 o1 l1) k1 \<and> Ang_inside (An k1 o1 l1) h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P6 : "Ang_inside (An k1 o1 l1) h1 \<Longrightarrow>
    Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An k1 o1 l1) h1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
by (simp add:Ang_sub_lemma1)
[PROOF STATE]
proof (state)
this:
Ang_inside (An k1 o1 l1) h1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P7 : "Plane_sameside (Li o1 l1) k1 h1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li o1 l1) k1 h1
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o1 l1) k1 h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P8 : "Plane_sameside (Li o2 l2) k2 h2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li o2 l2) k2 h2
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o2 l2) k2 h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P9 : "\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P7 P8 P9 P10
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Plane_sameside (Li o1 l1) k1 h1
Plane_sameside (Li o2 l2) k2 h2
\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)
[PROOF STEP]
have P11 : "Ang_inside (An h1 o1 l1) k1 \<Longrightarrow>
    Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_sameside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Plane_sameside (Li o1 l1) k1 h1
Plane_sameside (Li o2 l2) k2 h2
\<not> Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 h1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 h2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)
[PROOF STEP]
by (simp add:Ang_sub_lemma1)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P12 : "Eq (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P13 : "Eq (Geos (Ang (An k2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An k2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An k2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P11 P12
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)
Eq (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)
[PROOF STEP]
have P14 : "Ang_inside (An h1 o1 l1) k1 \<Longrightarrow>
    Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)
Eq (Geos (Ang (An k1 o1 h1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P13 P14
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An k2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)
[PROOF STEP]
have P15 : "Ang_inside (An h1 o1 l1) k1 \<Longrightarrow>
    Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An k2 o2 h2)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An k2 o2 h2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P5 P6 P15
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An h1 o1 l1) k1 \<and> \<not> Ang_inside (An k1 o1 l1) h1 \<or> \<not> Ang_inside (An h1 o1 l1) k1 \<and> Ang_inside (An k1 o1 l1) h1
Ang_inside (An k1 o1 l1) h1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An h1 o1 l1) k1 \<and> \<not> Ang_inside (An k1 o1 l1) h1 \<or> \<not> Ang_inside (An h1 o1 l1) k1 \<and> Ang_inside (An k1 o1 l1) h1
Ang_inside (An k1 o1 l1) h1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
Ang_inside (An h1 o1 l1) k1 \<Longrightarrow> Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Congruence_Rule) Ang_add :
  assumes
    "Plane_diffside (Li o1 l1) h1 k1"
    "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)"
    "Plane_diffside (Li o2 l2) h2 k2"
    "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)"
    "Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)"
    "Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)"
    "\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)"
    "\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)"
  shows
    "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have "\<exists>p. Bet_Point (Se h1 k1) p \<and> Line_on (Li o1 l1) p
    \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se h1 k1) p \<and> Line_on (Li o1 l1) p \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se h1 k1) p \<and> Line_on (Li o1 l1) p \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se h1 k1) p \<and> Line_on (Li o1 l1) p \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
[PROOF STEP]
obtain l11 :: Point where P1 : "Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11
    \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se h1 k1) p \<and> Line_on (Li o1 l1) p \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1

goal (1 subgoal):
 1. (\<And>l11. Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P2 : "Line_on (Li o1 l1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 l1) o1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 l1) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 l1) o1
[PROOF STEP]
have P3 : "Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 l1) o1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P1 P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P5 : "Line_on (Li o1 k1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 k1) o1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k1) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P6 : "Line_on (Li o1 k1) k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 k1) k1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k1) k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P4 P5 P6
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
Line_on (Li o1 k1) o1
Line_on (Li o1 k1) k1
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 p)) add Emp)
    \<and> Bet_Point (Se p k1) o1 \<and> Line_on (Li o1 k1) p \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
Line_on (Li o1 k1) o1
Line_on (Li o1 k1) k1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 p)) add Emp) \<and> Bet_Point (Se p k1) o1 \<and> Line_on (Li o1 k1) p \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain k11 :: Point where P7 : "Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp)
    \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 p)) add Emp) \<and> Bet_Point (Se p k1) o1 \<and> Line_on (Li o1 k1) p \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi p) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)
[PROOF STEP]
have P8 : "Bet_Point (Se k11 k1) o1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se k11 k1) o1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se k11 k1) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have "Line_on (Li k11 k1) k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li k11 k1) k1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li k11 k1) k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li k11 k1) k1
[PROOF STEP]
have P9 : "Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li k11 k1) k1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P1 P9
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P2 P8 P10
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 l1) o1
Bet_Point (Se k11 k1) o1
\<not> Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have "Plane_diffside (Li o1 l1) k11 k1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 l1) o1
Bet_Point (Se k11 k1) o1
\<not> Eq (Geos (Lin (Li k11 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li o1 l1) k11 k1
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li o1 l1) k11 k1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) k11 k1
[PROOF STEP]
have P11 : "Plane_diffside (Li o1 l1) k1 k11"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) k11 k1

goal (1 subgoal):
 1. Plane_diffside (Li o1 l1) k1 k11
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li o1 l1) k1 k11

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P12 : "Plane_diffside (Li o1 l1) k1 h1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li o1 l1) k1 h1
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li o1 l1) k1 h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 l1) o1
[PROOF STEP]
have P13 : "Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) h1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 l1) o1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P1 P13
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) h1
[PROOF STEP]
have P14 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) h1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P15 : "Line_on (Li o1 h1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 h1) o1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 h1) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P16 : "Line_on (Li o1 h1) h1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 h1) h1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 h1) h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P5 P14 P15 P16
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 k1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
Line_on (Li o1 h1) o1
Line_on (Li o1 h1) h1
[PROOF STEP]
have P17 : "Line_on (Li o1 k1) h1
    \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 k1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
Line_on (Li o1 h1) o1
Line_on (Li o1 h1) h1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P17
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Line_on (Li o1 k1) h1 \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
[PROOF STEP]
have P18 : "\<not> Line_on (Li o1 k1) h1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Line_on (Li o1 k1) h1 \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li o1 k1) h1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li o1 k1) h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)
[PROOF STEP]
have P19 : "Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) h1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) h1
[PROOF STEP]
by (blast intro:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P18 P19
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 k1) h1
Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) h1
[PROOF STEP]
have P20 : "\<not> Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 k1) h1
Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp) \<Longrightarrow> Line_on (Li o1 k1) h1

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P11 P12 P20
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) k1 k11
Plane_diffside (Li o1 l1) k1 h1
\<not> Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp)
[PROOF STEP]
have "Plane_sameside (Li o1 l1) k11 h1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) k1 k11
Plane_diffside (Li o1 l1) k1 h1
\<not> Eq (Geos (Poi k11) add Emp) (Geos (Poi h1) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li o1 l1) k11 h1
[PROOF STEP]
by (blast intro:Plane_trans_inv)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o1 l1) k11 h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o1 l1) k11 h1
[PROOF STEP]
have P21 : "Plane_sameside (Li o1 l1) h1 k11"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o1 l1) k11 h1

goal (1 subgoal):
 1. Plane_sameside (Li o1 l1) h1 k11
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o1 l1) h1 k11

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have "\<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p
    \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
[PROOF STEP]
obtain l21 :: Point where P22 : "Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21
    \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. (\<And>l21. Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P23 : "Line_on (Li o2 l2) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 l2) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 l2) o2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 l2) o2
[PROOF STEP]
have P24 : "Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 l2) o2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P22 P24
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2
[PROOF STEP]
have P25 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P26 : "Line_on (Li o2 k2) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 k2) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 k2) o2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P27 : "Line_on (Li o2 k2) k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 k2) k2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 k2) k2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P4 P25 P26 P27
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Line_on (Li o2 k2) o2
Line_on (Li o2 k2) k2
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp)
    \<and> Bet_Point (Se p k2) o2 \<and> Line_on (Li o2 k2) p \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Line_on (Li o2 k2) o2
Line_on (Li o2 k2) k2

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp) \<and> Bet_Point (Se p k2) o2 \<and> Line_on (Li o2 k2) p \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by (simp add:Seg_move_diffside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp) \<and> Bet_Point (Se p k2) o2 \<and> Line_on (Li o2 k2) p \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp) \<and> Bet_Point (Se p k2) o2 \<and> Line_on (Li o2 k2) p \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain k21 :: Point where P28 : "Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp)
    \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp) \<and> Bet_Point (Se p k2) o2 \<and> Line_on (Li o2 k2) p \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>k21. Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P28
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
[PROOF STEP]
have P29 : "Bet_Point (Se k21 k2) o2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se k21 k2) o2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se k21 k2) o2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have "Line_on (Li k21 k2) k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li k21 k2) k2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li k21 k2) k2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li k21 k2) k2
[PROOF STEP]
have P30 : "Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li k21 k2) k2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have "\<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p
    \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se h2 k2) p \<and> Line_on (Li o2 l2) p \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P22 P30
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2
[PROOF STEP]
have P31 : "\<not> Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp) \<Longrightarrow> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P23 P29 P31
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 l2) o2
Bet_Point (Se k21 k2) o2
\<not> Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)
[PROOF STEP]
have "Plane_diffside (Li o2 l2) k21 k2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 l2) o2
Bet_Point (Se k21 k2) o2
\<not> Eq (Geos (Lin (Li k21 k2)) add Emp) (Geos (Lin (Li o2 l2)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li o2 l2) k21 k2
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li o2 l2) k21 k2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o2 l2) k21 k2
[PROOF STEP]
have P32 : "Plane_diffside (Li o2 l2) k2 k21"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o2 l2) k21 k2

goal (1 subgoal):
 1. Plane_diffside (Li o2 l2) k2 k21
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li o2 l2) k2 k21

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P33 : "Plane_diffside (Li o2 l2) k2 h2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li o2 l2) k2 h2
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li o2 l2) k2 h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P23
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 l2) o2
[PROOF STEP]
have P34 : "Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 l2) h2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 l2) o2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P22 P34
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 l2) h2
[PROOF STEP]
have P35 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 l2) h2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P36 : "Line_on (Li o2 h2) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 h2) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 h2) o2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P37 : "Line_on (Li o2 h2) h2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 h2) h2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 h2) h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P26 P35 P36 P37
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 k2) o2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Line_on (Li o2 h2) o2
Line_on (Li o2 h2) h2
[PROOF STEP]
have P38 : "Line_on (Li o2 k2) h2
    \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 k2) o2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Line_on (Li o2 h2) o2
Line_on (Li o2 h2) h2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P38
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Line_on (Li o2 k2) h2 \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P39 : "\<not> Line_on (Li o2 k2) h2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Line_on (Li o2 k2) h2 \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li o2 k2) h2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li o2 k2) h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P28
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
[PROOF STEP]
have P40 : "Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h2
[PROOF STEP]
by (blast intro:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P39 P40
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 k2) h2
Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h2
[PROOF STEP]
have P41 : "\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 k2) h2
Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h2

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P32 P33 P41
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o2 l2) k2 k21
Plane_diffside (Li o2 l2) k2 h2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp)
[PROOF STEP]
have "Plane_sameside (Li o2 l2) k21 h2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o2 l2) k2 k21
Plane_diffside (Li o2 l2) k2 h2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h2) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li o2 l2) k21 h2
[PROOF STEP]
by (blast intro:Plane_trans_inv)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o2 l2) k21 h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o2 l2) k21 h2
[PROOF STEP]
have P42 : "Plane_sameside (Li o2 l2) h2 k21"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o2 l2) k21 h2

goal (1 subgoal):
 1. Plane_sameside (Li o2 l2) h2 k21
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li o2 l2) h2 k21

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1
[PROOF STEP]
have "Def (Ang (An o1 l1 k1))"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Bet_Point (Se h1 k1) l11 \<and> Line_on (Li o1 l1) l11 \<and> \<not> Line_on (Li o1 l1) h1 \<and> \<not> Line_on (Li o1 l1) k1

goal (1 subgoal):
 1. Def (Ang (An o1 l1 k1))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o1 l1 k1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 l1 k1))
[PROOF STEP]
have P43 : "Def (Ang (An k1 o1 l1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 l1 k1))

goal (1 subgoal):
 1. Def (Ang (An k1 o1 l1))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An k1 o1 l1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P22
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2
[PROOF STEP]
have "Def (Ang (An o2 l2 k2))"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Bet_Point (Se h2 k2) l21 \<and> Line_on (Li o2 l2) l21 \<and> \<not> Line_on (Li o2 l2) h2 \<and> \<not> Line_on (Li o2 l2) k2

goal (1 subgoal):
 1. Def (Ang (An o2 l2 k2))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o2 l2 k2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o2 l2 k2))
[PROOF STEP]
have P44 : "Def (Ang (An k2 o2 l2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o2 l2 k2))

goal (1 subgoal):
 1. Def (Ang (An k2 o2 l2))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An k2 o2 l2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k11 k1) o1
[PROOF STEP]
have P45 : "Bet_Point (Se k1 k11) o1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k11 k1) o1

goal (1 subgoal):
 1. Bet_Point (Se k1 k11) o1
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se k1 k11) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P28
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
[PROOF STEP]
have P46 : "Bet_Point (Se k2 k21) o2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se k2 k21) o2
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se k2 k21) o2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P43 P44 P45 P46
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Def (Ang (An k1 o1 l1))
Def (Ang (An k2 o2 l2))
Bet_Point (Se k1 k11) o1
Bet_Point (Se k2 k21) o2
[PROOF STEP]
have P47 : "Cong (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Def (Ang (An k1 o1 l1))
Def (Ang (An k2 o2 l2))
Bet_Point (Se k1 k11) o1
Bet_Point (Se k2 k21) o2

goal (1 subgoal):
 1. Cong (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)
[PROOF STEP]
by (simp add:Ang_complementary)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P48 : "Eq (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 l1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 l1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P49 : "Eq (Geos (Ang (An l2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An l2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An l2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P47 P48
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)
Eq (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 l1)) add Emp)
[PROOF STEP]
have P50 : "Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)
Eq (Geos (Ang (An l1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 l1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P49 P50
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An l2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)
Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)
[PROOF STEP]
have P51 : "Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An l2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)
Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An l2 o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P52 : "Line_on (Li o1 k11) k11"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 k11) k11
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k11) k11

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P53 : "Line_on (Li o1 k11) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o1 k11) o1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k11) o1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P5 P7 P52 P53
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o1 k1) o1
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)
Line_on (Li o1 k11) k11
Line_on (Li o1 k11) o1
[PROOF STEP]
have P54 : "Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o1 k1) o1
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)
Line_on (Li o1 k11) k11
Line_on (Li o1 k11) o1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)
[PROOF STEP]
by (blast intro:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P54
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)
[PROOF STEP]
have P55 : "Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)
    \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P55
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
[PROOF STEP]
have P56 : "\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P57 : "Line_on (Li o2 k21) k21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 k21) k21
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 k21) k21

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P58 : "Line_on (Li o2 k21) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li o2 k21) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 k21) o2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P26 P28 P57 P58
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li o2 k2) o2
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
Line_on (Li o2 k21) k21
Line_on (Li o2 k21) o2
[PROOF STEP]
have P59 : "Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li o2 k2) o2
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
Line_on (Li o2 k21) k21
Line_on (Li o2 k21) o2

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)
[PROOF STEP]
by (blast intro:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P59
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)
[PROOF STEP]
have P60 : "Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)
    \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P60
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P61 : "\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from assms P21 P42 P51 P56 P61
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Plane_sameside (Li o1 l1) h1 k11
Plane_sameside (Li o2 l2) h2 k21
Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)
[PROOF STEP]
have P62 : "Cong (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li o1 l1) h1 k1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi l1) add Emp)
Plane_diffside (Li o2 l2) h2 k2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
Cong (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k2 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k1)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
Plane_sameside (Li o1 l1) h1 k11
Plane_sameside (Li o2 l2) h2 k21
Cong (Geos (Ang (An k11 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l2)) add Emp)
\<not> Eq (Geos (Lin (Li o1 h1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)
\<not> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)
[PROOF STEP]
by (simp add:Ang_sub)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P63 : "Eq (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 h1)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 h1)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
have P64 : "Eq (Geos (Ang (An h2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An h2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P62 P63
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)
Eq (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 h1)) add Emp)
[PROOF STEP]
have P65 : "Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)
Eq (Geos (Ang (An h1 o1 k11)) add Emp) (Geos (Ang (An k11 o1 h1)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P64 P65
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An h2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)
Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)
[PROOF STEP]
have P66 : "Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An h2 o2 k21)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)
Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An h2 o2 k21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P54
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)
[PROOF STEP]
have P67 : "Line_on (Li o1 k11) h1 \<Longrightarrow> Line_on (Li o1 k1) h1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o1 k1)) add Emp) (Geos (Lin (Li o1 k11)) add Emp)

goal (1 subgoal):
 1. Line_on (Li o1 k11) h1 \<Longrightarrow> Line_on (Li o1 k1) h1
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 k11) h1 \<Longrightarrow> Line_on (Li o1 k1) h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P18 P67
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 k1) h1
Line_on (Li o1 k11) h1 \<Longrightarrow> Line_on (Li o1 k1) h1
[PROOF STEP]
have P68 : "\<not> Line_on (Li o1 k11) h1"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 k1) h1
Line_on (Li o1 k11) h1 \<Longrightarrow> Line_on (Li o1 k1) h1

goal (1 subgoal):
 1. \<not> Line_on (Li o1 k11) h1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li o1 k11) h1

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P7 P68
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)
\<not> Line_on (Li o1 k11) h1
[PROOF STEP]
have "Def (Ang (An o1 k11 h1))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o1 k11)) add Emp) \<and> Bet_Point (Se k11 k1) o1 \<and> Line_on (Li o1 k1) k11 \<and> \<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k11) add Emp)
\<not> Line_on (Li o1 k11) h1

goal (1 subgoal):
 1. Def (Ang (An o1 k11 h1))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o1 k11 h1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 k11 h1))
[PROOF STEP]
have P69 : "Def (Ang (An k11 o1 h1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 k11 h1))

goal (1 subgoal):
 1. Def (Ang (An k11 o1 h1))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An k11 o1 h1))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P59
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)
[PROOF STEP]
have P70 : "Line_on (Li o2 k21) h2 \<Longrightarrow> Line_on (Li o2 k2) h2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o2 k2)) add Emp) (Geos (Lin (Li o2 k21)) add Emp)

goal (1 subgoal):
 1. Line_on (Li o2 k21) h2 \<Longrightarrow> Line_on (Li o2 k2) h2
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 k21) h2 \<Longrightarrow> Line_on (Li o2 k2) h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P39 P70
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o2 k2) h2
Line_on (Li o2 k21) h2 \<Longrightarrow> Line_on (Li o2 k2) h2
[PROOF STEP]
have P71 : "\<not> Line_on (Li o2 k21) h2"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o2 k2) h2
Line_on (Li o2 k21) h2 \<Longrightarrow> Line_on (Li o2 k2) h2

goal (1 subgoal):
 1. \<not> Line_on (Li o2 k21) h2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li o2 k21) h2

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P28 P71
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
\<not> Line_on (Li o2 k21) h2
[PROOF STEP]
have "Def (Ang (An o2 k21 h2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Bet_Point (Se k21 k2) o2 \<and> Line_on (Li o2 k2) k21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
\<not> Line_on (Li o2 k21) h2

goal (1 subgoal):
 1. Def (Ang (An o2 k21 h2))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An o2 k21 h2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o2 k21 h2))
[PROOF STEP]
have P72 : "Def (Ang (An k21 o2 h2))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o2 k21 h2))

goal (1 subgoal):
 1. Def (Ang (An k21 o2 h2))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An k21 o2 h2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
from P8 P29 P66 P69 P72
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k11 k1) o1
Bet_Point (Se k21 k2) o2
Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)
Def (Ang (An k11 o1 h1))
Def (Ang (An k21 o2 h2))
[PROOF STEP]
show "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k11 k1) o1
Bet_Point (Se k21 k2) o2
Cong (Geos (Ang (An k11 o1 h1)) add Emp) (Geos (Ang (An k21 o2 h2)) add Emp)
Def (Ang (An k11 o1 h1))
Def (Ang (An k21 o2 h2))

goal (1 subgoal):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
[PROOF STEP]
by (simp add:Ang_complementary)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed