[STATEMENT]
lemma (in Congruence_Rule) Ang_sub_lemma1 :
  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)"
    "Ang_inside (An k1 o1 l1) h1"
  shows
    "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)"
    "Ang_inside (An k2 o2 l2) h2"
[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) &&& Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[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)
Ang_inside (An k1 o1 l1) h1

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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
\<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)
Ang_inside (An k1 o1 l1) h1
\<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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[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)
Ang_inside (An k1 o1 l1) h1

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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
\<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)
Ang_inside (An k1 o1 l1) h1
\<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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[PROOF STEP]
have P5 : "\<not> Line_on (Li o2 l2) 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)
Ang_inside (An k1 o1 l1) h1

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P5
[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)
Ang_inside (An k1 o1 l1) h1
\<not> Line_on (Li o2 l2) h2
[PROOF STEP]
have "Def (Ang (An o2 l2 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)
Ang_inside (An k1 o1 l1) h1
\<not> Line_on (Li o2 l2) h2

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[PROOF STEP]
have P7 : "\<not> Line_on (Li o2 l2) k2"
[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)
Ang_inside (An k1 o1 l1) h1

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P7
[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)
Ang_inside (An k1 o1 l1) h1
\<not> Line_on (Li o2 l2) k2
[PROOF STEP]
have "Def (Ang (An o2 l2 k2))"
[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)
Ang_inside (An k1 o1 l1) h1
\<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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o2 l2 k2))
[PROOF STEP]
have P8 : "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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P4 P8
[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)
Ang_inside (An k1 o1 l1) h1
Def (Ang (An k1 o1 l1))
Def (Ang (An k2 o2 l2))
[PROOF STEP]
have "\<exists>p q. Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An p o2 q)) add Emp)
    \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An p o2 q)) add Emp)
    \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp) \<and> Line_on (Li o2 k2) p \<and> \<not> Bet_Point (Se p k2) o2
    \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 q)) add Emp) \<and> Line_on (Li o2 l2) q \<and> \<not> Bet_Point (Se q l2) o2 \<and> Def (Ang (An p o2 q))"
[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)
Ang_inside (An k1 o1 l1) h1
Def (Ang (An k1 o1 l1))
Def (Ang (An k2 o2 l2))

goal (1 subgoal):
 1. \<exists>p q. Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An p o2 q)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An p o2 q)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp) \<and> Line_on (Li o2 k2) p \<and> \<not> Bet_Point (Se p k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 q)) add Emp) \<and> Line_on (Li o2 l2) q \<and> \<not> Bet_Point (Se q l2) o2 \<and> Def (Ang (An p o2 q))
[PROOF STEP]
by (simp add:Ang_replace)
[PROOF STATE]
proof (state)
this:
\<exists>p q. Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An p o2 q)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An p o2 q)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 p)) add Emp) \<and> Line_on (Li o2 k2) p \<and> \<not> Bet_Point (Se p k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 q)) add Emp) \<and> Line_on (Li o2 l2) q \<and> \<not> Bet_Point (Se q l2) o2 \<and> Def (Ang (An p o2 q))

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[PROOF STEP]
have "Plane_diffside (Li o1 h1) k1 l1"
[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)
Ang_inside (An k1 o1 l1) h1

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

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

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
[PROOF STEP]
have "Eq (Geos (Poi h11) add Emp) (Geos (Poi o1) add Emp) \<Longrightarrow>
    Bet_Point (Se k1 l1) o1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1

goal (1 subgoal):
 1. Eq (Geos (Poi h11) add Emp) (Geos (Poi o1) add Emp) \<Longrightarrow> Bet_Point (Se k1 l1) o1
[PROOF STEP]
by (blast intro:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi h11) add Emp) (Geos (Poi o1) add Emp) \<Longrightarrow> Bet_Point (Se k1 l1) o1

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P3 P11
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 l1) k1
Eq (Geos (Poi h11) add Emp) (Geos (Poi o1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1
[PROOF STEP]
have P12 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h11) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 l1) k1
Eq (Geos (Poi h11) add Emp) (Geos (Poi o1) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P13 : "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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P14 : "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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h2 o2 l2))
[PROOF STEP]
have "\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi o2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h2 o2 l2))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi o2) add Emp)
[PROOF STEP]
have P15 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi o2) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P12 P13 P14 P15
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h11) add Emp)
Line_on (Li o2 h2) o2
Line_on (Li o2 h2) h2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 p)) add Emp)
    \<and> \<not> Bet_Point (Se p h2) o2 \<and> Line_on (Li o2 h2) 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 h11) add Emp)
Line_on (Li o2 h2) o2
Line_on (Li o2 h2) h2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P17 : "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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have "Line_on (Li h1 h11) h1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li h1 h11) h1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li h1 h11) h1

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

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

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

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

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

goal (1 subgoal):
 1. Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 h11
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 h11

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 h11
[PROOF STEP]
have P20 : "Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h11 h1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 h11

goal (1 subgoal):
 1. Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h11 h1
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h11 h1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
[PROOF STEP]
have P21 : "Bet_Point (Se l1 k1) h11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li l1 k1) k1
[PROOF STEP]
have P23 : "Eq (Geos (Lin (Li l1 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 l1 k1) k1

goal (1 subgoal):
 1. Eq (Geos (Lin (Li l1 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 l1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P3 P23
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li o1 l1) k1
Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp) \<Longrightarrow> Line_on (Li o1 l1) k1
[PROOF STEP]
have P24 : "\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li o1 l1) k1
Eq (Geos (Lin (Li l1 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 l1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P21 P22 P24
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se l1 k1) h11
Line_on (Li o1 l1) l1
\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)
[PROOF STEP]
have P25 : "Plane_sameside (Li o1 l1) h11 k1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se l1 k1) h11
Line_on (Li o1 l1) l1
\<not> Eq (Geos (Lin (Li l1 k1)) add Emp) (Geos (Lin (Li o1 l1)) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P20 P25
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h11 h1
Plane_sameside (Li o1 l1) h11 k1
[PROOF STEP]
have "Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 k1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h11 h1
Plane_sameside (Li o1 l1) h11 k1

goal (1 subgoal):
 1. Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 k1
[PROOF STEP]
by (simp add:Plane_trans Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 k1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 k1
[PROOF STEP]
have P26 : "Bet_Point (Se h1 h11) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 l1) h1 k1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> Plane_diffside (Li o1 l1) h1 k1

goal (1 subgoal):
 1. Bet_Point (Se h1 h11) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 l1) h1 k1
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h1 h11) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 l1) h1 k1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P26
[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)
Ang_inside (An k1 o1 l1) h1
Bet_Point (Se h1 h11) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 l1) h1 k1
[PROOF STEP]
have P27 : "\<not> Bet_Point (Se h1 h11) o1"
[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)
Ang_inside (An k1 o1 l1) h1
Bet_Point (Se h1 h11) o1 \<Longrightarrow> \<not> Plane_sameside (Li o1 l1) h1 k1

goal (1 subgoal):
 1. \<not> Bet_Point (Se h1 h11) o1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se h1 h11) o1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P28 : "\<not> Bet_Point (Se l1 l1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se l1 l1) o1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se l1 l1) o1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P2 P10 P22 P27 P28 P12
[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)
Ang_inside (An k1 o1 l1) h1
Def (Ang (An h1 o1 l1))
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
Line_on (Li o1 l1) l1
\<not> Bet_Point (Se h1 h11) o1
\<not> Bet_Point (Se l1 l1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h11) add Emp)
[PROOF STEP]
have P29 : "Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h11 o1 l1)) add Emp) \<and> Def (Ang (An h11 o1 l1))"
[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)
Ang_inside (An k1 o1 l1) h1
Def (Ang (An h1 o1 l1))
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
Line_on (Li o1 l1) l1
\<not> Bet_Point (Se h1 h11) o1
\<not> Bet_Point (Se l1 l1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h11) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h11 o1 l1)) add Emp) \<and> Def (Ang (An h11 o1 l1))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h11 o1 l1)) add Emp) \<and> Def (Ang (An h11 o1 l1))

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
have P31 : "\<not> Bet_Point (Se h2 h21) o2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
[PROOF STEP]
have P32 : "\<not> Bet_Point (Se l2 l21) o2"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P6 P9 P16 P30 P31 P32
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
\<not> Bet_Point (Se h2 h21) o2
\<not> Bet_Point (Se l2 l21) o2
[PROOF STEP]
have P33 : "Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h2 o2 l2))
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
\<not> Bet_Point (Se h2 h21) o2
\<not> Bet_Point (Se l2 l21) o2

goal (1 subgoal):
 1. Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P29
[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)
Ang_inside (An k1 o1 l1) h1
Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h11 o1 l1)) add Emp) \<and> Def (Ang (An h11 o1 l1))
[PROOF STEP]
have P34 : "Cong (Geos (Ang (An h11 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) 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)
Ang_inside (An k1 o1 l1) h1
Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h11 o1 l1)) add Emp) \<and> Def (Ang (An h11 o1 l1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P33 P34
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))
Cong (Geos (Ang (An h11 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)
[PROOF STEP]
have P35 : "Cong (Geos (Ang (An h11 o1 l1)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))
Cong (Geos (Ang (An h11 o1 l1)) add Emp) (Geos (Ang (An h2 o2 l2)) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P29
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h11 o1 l1)) add Emp) \<and> Def (Ang (An h11 o1 l1))
[PROOF STEP]
have "Def (Tri (Tr h11 o1 l1))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An h1 o1 l1)) add Emp) (Geos (Ang (An h11 o1 l1)) add Emp) \<and> Def (Ang (An h11 o1 l1))

goal (1 subgoal):
 1. Def (Tri (Tr h11 o1 l1))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr h11 o1 l1))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr h11 o1 l1))
[PROOF STEP]
have P36 : "Def (Tri (Tr o1 h11 l1))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr h11 o1 l1))

goal (1 subgoal):
 1. Def (Tri (Tr o1 h11 l1))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr o1 h11 l1))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P33
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))
[PROOF STEP]
have "Def (Tri (Tr h21 o2 l21))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))

goal (1 subgoal):
 1. Def (Tri (Tr h21 o2 l21))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr h21 o2 l21))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr h21 o2 l21))
[PROOF STEP]
have P37 : "Def (Tri (Tr o2 h21 l21))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr h21 o2 l21))

goal (1 subgoal):
 1. Def (Tri (Tr o2 h21 l21))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr o2 h21 l21))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9 P16 P35 P36 P37
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
Cong (Geos (Ang (An h11 o1 l1)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp)
Def (Tri (Tr o1 h11 l1))
Def (Tri (Tr o2 h21 l21))
[PROOF STEP]
have P38 : "Cong (Geos (Tri (Tr o1 h11 l1)) add Emp) (Geos (Tri (Tr o2 h21 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
Cong (Geos (Ang (An h11 o1 l1)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp)
Def (Tri (Tr o1 h11 l1))
Def (Tri (Tr o2 h21 l21))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr o1 h11 l1)) add Emp) (Geos (Tri (Tr o2 h21 l21)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr o1 h11 l1)) add Emp) (Geos (Tri (Tr o2 h21 l21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr o1 h11 l1)) add Emp) (Geos (Tri (Tr o2 h21 l21)) add Emp)
[PROOF STEP]
have P39 : "Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An o2 l21 h21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr o1 h11 l1)) add Emp) (Geos (Tri (Tr o2 h21 l21)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An o2 l21 h21)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An o2 l21 h21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An k1 o1 l1))
[PROOF STEP]
have P40 : "Def (Tri (Tr o1 k1 l1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An k1 o1 l1))

goal (1 subgoal):
 1. Def (Tri (Tr o1 k1 l1))
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr o1 k1 l1))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
[PROOF STEP]
have P41 : "Def (Tri (Tr o2 k21 l21))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))

goal (1 subgoal):
 1. Def (Tri (Tr o2 k21 l21))
[PROOF STEP]
by (simp add:Ang_to_Tri Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr o2 k21 l21))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9 P40 P41
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Def (Tri (Tr o1 k1 l1))
Def (Tri (Tr o2 k21 l21))
[PROOF STEP]
have P42 : "Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Def (Tri (Tr o1 k1 l1))
Def (Tri (Tr o2 k21 l21))

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)
[PROOF STEP]
have P43 : "Cong (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o2 l21 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)

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

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P46 : "\<not> Bet_Point (Se o1 o1) l1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se o1 o1) l1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se o1 o1) l1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
[PROOF STEP]
have P47 : "Line_on (Li l1 k1) h11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1

goal (1 subgoal):
 1. Line_on (Li l1 k1) h11
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li l1 k1) h11

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
[PROOF STEP]
have "Inv(Bet_Point (Se h11 k1) l1)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1

goal (1 subgoal):
 1. Inv (Bet_Point (Se h11 k1) l1)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se h11 k1) l1)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se h11 k1) l1)
[PROOF STEP]
have "\<not> Bet_Point (Se h11 k1) l1"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se h11 k1) l1)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se h11 k1) l1
[PROOF STEP]
have P48 : "\<not> Bet_Point (Se k1 h11) l1"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se h11 k1) l1

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[PROOF STEP]
have P49 : "\<not> Eq (Geos (Poi l1) add Emp) (Geos (Poi o1) 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)
Ang_inside (An k1 o1 l1) h1

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
[PROOF STEP]
have "Bet_Point (Se k1 l1) h11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1

goal (1 subgoal):
 1. Bet_Point (Se k1 l1) h11
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se k1 l1) h11

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11
[PROOF STEP]
have P50 : "\<not> Eq (Geos (Poi l1) add Emp) (Geos (Poi h11) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P44 P45 P46 P47 P48 P49 P50
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An o1 l1 k1))
Line_on (Li l1 o1) o1
\<not> Bet_Point (Se o1 o1) l1
Line_on (Li l1 k1) h11
\<not> Bet_Point (Se k1 h11) l1
\<not> Eq (Geos (Poi l1) add Emp) (Geos (Poi o1) add Emp)
\<not> Eq (Geos (Poi l1) add Emp) (Geos (Poi h11) add Emp)
[PROOF STEP]
have P51 : "Eq (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o1 l1 h11)) add Emp) \<and> Def (Ang (An o1 l1 h11))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An o1 l1 k1))
Line_on (Li l1 o1) o1
\<not> Bet_Point (Se o1 o1) l1
Line_on (Li l1 k1) h11
\<not> Bet_Point (Se k1 h11) l1
\<not> Eq (Geos (Poi l1) add Emp) (Geos (Poi o1) add Emp)
\<not> Eq (Geos (Poi l1) add Emp) (Geos (Poi h11) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o1 l1 h11)) add Emp) \<and> Def (Ang (An o1 l1 h11))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o1 l1 h11)) add Emp) \<and> Def (Ang (An o1 l1 h11))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P43 P52
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o2 l21 k21)) add Emp)
Eq (Geos (Ang (An o2 l21 k21)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)
[PROOF STEP]
have P53 : "Cong (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o2 l21 k21)) add Emp)
Eq (Geos (Ang (An o2 l21 k21)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P51 P53
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o1 l1 h11)) add Emp) \<and> Def (Ang (An o1 l1 h11))
Cong (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)
[PROOF STEP]
have P54 : "Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An o1 l1 h11)) add Emp) \<and> Def (Ang (An o1 l1 h11))
Cong (Geos (Ang (An o1 l1 k1)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P39 P55
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An o2 l21 h21)) add Emp)
Eq (Geos (Ang (An o2 l21 h21)) add Emp) (Geos (Ang (An h21 l21 o2)) add Emp)
[PROOF STEP]
have P56 : "Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An h21 l21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An o2 l21 h21)) add Emp)
Eq (Geos (Ang (An o2 l21 h21)) add Emp) (Geos (Ang (An h21 l21 o2)) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P57 : "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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P58 : "Line_on (Li l21 o2) o2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li l21 o2) o2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li l21 o2) o2

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
[PROOF STEP]
have P60 : "Line_on (Li o2 l2) l21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))

goal (1 subgoal):
 1. Line_on (Li o2 l2) l21
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 l2) l21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P30 P57 P58 P59 P60
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
Line_on (Li o2 l2) o2
Line_on (Li l21 o2) o2
Line_on (Li l21 o2) l21
Line_on (Li o2 l2) l21
[PROOF STEP]
have P61 : "Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
Line_on (Li o2 l2) o2
Line_on (Li l21 o2) o2
Line_on (Li l21 o2) l21
Line_on (Li o2 l2) l21

goal (1 subgoal):
 1. Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P16 P57
[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)
Ang_inside (An k1 o1 l1) h1
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
Line_on (Li o2 l2) o2
[PROOF STEP]
have P62 : "\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) h21 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)
Ang_inside (An k1 o1 l1) h1
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
Line_on (Li o2 l2) o2

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h21 h2
[PROOF STEP]
by (blast intro:Plane_sameside_HalfLine Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h21 h2

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[PROOF STEP]
have P63 : "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)
Ang_inside (An k1 o1 l1) h1

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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P41
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr o2 k21 l21))
[PROOF STEP]
have P64 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr o2 k21 l21))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9 P57 P63 P64
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Line_on (Li o2 l2) o2
Plane_sameside (Li o2 l2) k2 h2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
[PROOF STEP]
have P65 : "\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k2 k21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Line_on (Li o2 l2) o2
Plane_sameside (Li o2 l2) k2 h2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P62
[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)
Ang_inside (An k1 o1 l1) h1
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h21 h2
[PROOF STEP]
have P67 : "\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) h21 k2"
[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)
Ang_inside (An k1 o1 l1) h1
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h21 h2

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) h21 k2
[PROOF STEP]
by (blast intro:Plane_sameside_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) h21 k2

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P68 : "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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
[PROOF STEP]
have P69 : "Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9 P13 P16 P68 P69
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Line_on (Li o2 h2) o2
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
Line_on (Li o2 k2) o2
Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h21
[PROOF STEP]
have P70 : "Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
Line_on (Li o2 h2) o2
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
Line_on (Li o2 k2) o2
Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Line_on (Li o2 k2) h21

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P70
[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)
Ang_inside (An k1 o1 l1) h1
Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li o2 h2)) add Emp) (Geos (Lin (Li o2 k2)) add Emp)
[PROOF STEP]
have P71 : "\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) 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)
Ang_inside (An k1 o1 l1) h1
Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) 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 (Poi k21) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P65 P67 P71
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) k2 k21
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) h21 k2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
have P72 : "\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) k2 k21
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) h21 k2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
by (blast intro:Plane_sameside_trans Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P66
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) k21 k2
[PROOF STEP]
have P73 : "\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) k21 k2

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P71 P72 P73
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
have P74 : "\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi h21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P63
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li o2 l2) k2 h2
[PROOF STEP]
have P75 : "Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k2 h21"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li o2 l2) k2 h2

goal (1 subgoal):
 1. \<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k2 h21
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k2 h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P66 P71 P75
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) k21 k2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k2 h21
[PROOF STEP]
have P76 : "Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) k21 k2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k2 h21

goal (1 subgoal):
 1. \<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
by (blast intro:Plane_sameside_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[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)
Ang_inside (An k1 o1 l1) h1
[PROOF STEP]
have P77 : "Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) h2 k21"
[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)
Ang_inside (An k1 o1 l1) h1

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P62 P71 P77
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h21 h2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h2 k21
[PROOF STEP]
have P78 : "\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h21 h2
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h2 k21

goal (1 subgoal):
 1. \<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
by (blast intro:Plane_sameside_trans Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P77
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h2 k21
[PROOF STEP]
have P79 : "Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp) \<Longrightarrow>
    Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow>
    Plane_sameside (Li o2 l2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp) \<Longrightarrow> Plane_sameside (Li o2 l2) h2 k21

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P71 P74 P76 P78 P79
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
have P80 : "Plane_sameside (Li o2 l2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
\<lbrakk>Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P61 P74 P80
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
Plane_sameside (Li o2 l2) k21 h21
[PROOF STEP]
have P81 : "Plane_sameside (Li l21 o2) k21 h21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li o2 l2)) add Emp) (Geos (Lin (Li l21 o2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
Plane_sameside (Li o2 l2) k21 h21

goal (1 subgoal):
 1. Plane_sameside (Li l21 o2) k21 h21
[PROOF STEP]
by (simp add:Plane_Line_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li l21 o2) k21 h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P54 P56 P74 P81
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)
Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An h21 l21 o2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
Plane_sameside (Li l21 o2) k21 h21
[PROOF STEP]
have P82 : "Eq (Geos (Lin (Li k21 l21)) add Emp) (Geos (Lin (Li h21 l21)) add Emp) \<and> \<not> Bet_Point (Se k21 h21) l21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An k21 l21 o2)) add Emp)
Cong (Geos (Ang (An o1 l1 h11)) add Emp) (Geos (Ang (An h21 l21 o2)) add Emp)
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
Plane_sameside (Li l21 o2) k21 h21

goal (1 subgoal):
 1. Eq (Geos (Lin (Li k21 l21)) add Emp) (Geos (Lin (Li h21 l21)) add Emp) \<and> \<not> Bet_Point (Se k21 h21) l21
[PROOF STEP]
by (simp add:Ang_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li k21 l21)) add Emp) (Geos (Lin (Li h21 l21)) add Emp) \<and> \<not> Bet_Point (Se k21 h21) l21

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P74 P82 P83
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
Eq (Geos (Lin (Li k21 l21)) add Emp) (Geos (Lin (Li h21 l21)) add Emp) \<and> \<not> Bet_Point (Se k21 h21) l21
Line_on (Li h21 l21) h21
[PROOF STEP]
have P84 : "Line_on (Li k21 l21) h21"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Eq (Geos (Poi h2) add Emp) (Geos (Poi h21) add Emp); \<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi k21) add Emp)\<rbrakk> \<Longrightarrow> Plane_sameside (Li o2 l2) k21 h21
Eq (Geos (Lin (Li k21 l21)) add Emp) (Geos (Lin (Li h21 l21)) add Emp) \<and> \<not> Bet_Point (Se k21 h21) l21
Line_on (Li h21 l21) h21

goal (1 subgoal):
 1. Line_on (Li k21 l21) h21
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li k21 l21) h21

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

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi k21) add Emp)
[PROOF STEP]
have P87 : "\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi l21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi k21) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P33
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))
[PROOF STEP]
have P88 : "\<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi h21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An h2 o2 l2)) add Emp) (Geos (Ang (An h21 o2 l21)) add Emp) \<and> Def (Ang (An h21 o2 l21))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P71
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
have P89 : "\<not> Eq (Geos (Poi h21) add Emp) (Geos (Poi k21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P81
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li l21 o2) k21 h21
[PROOF STEP]
have P90 : "\<not> Line_on (Li l21 o2) k21"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li l21 o2) k21 h21

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P90 P91
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li l21 o2) k21
Eq (Geos (Lin (Li k21 l21)) add Emp) (Geos (Lin (Li l21 o2)) add Emp) \<Longrightarrow> Line_on (Li l21 o2) k21
[PROOF STEP]
have P92 : "\<not> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li k21 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li l21 o2) k21
Eq (Geos (Lin (Li k21 l21)) add Emp) (Geos (Lin (Li l21 o2)) add Emp) \<Longrightarrow> Line_on (Li l21 o2) k21

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P59 P81 P84 P85 P86 P87 P88 P89 P92
[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)
Ang_inside (An k1 o1 l1) h1
Line_on (Li l21 o2) l21
Plane_sameside (Li l21 o2) k21 h21
Line_on (Li k21 l21) h21
Line_on (Li k21 l21) k21
Line_on (Li k21 l21) l21
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi l21) add Emp)
\<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi h21) add Emp)
\<not> Eq (Geos (Poi h21) add Emp) (Geos (Poi k21) add Emp)
\<not> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li k21 l21)) add Emp)
[PROOF STEP]
have P93 : "Bet_Point (Se h21 l21) k21 \<or> Bet_Point (Se l21 k21) h21"
[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)
Ang_inside (An k1 o1 l1) h1
Line_on (Li l21 o2) l21
Plane_sameside (Li l21 o2) k21 h21
Line_on (Li k21 l21) h21
Line_on (Li k21 l21) k21
Line_on (Li k21 l21) l21
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi l21) add Emp)
\<not> Eq (Geos (Poi l21) add Emp) (Geos (Poi h21) add Emp)
\<not> Eq (Geos (Poi h21) add Emp) (Geos (Poi k21) add Emp)
\<not> Eq (Geos (Lin (Li l21 o2)) add Emp) (Geos (Lin (Li k21 l21)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se h21 l21) k21 \<or> Bet_Point (Se l21 k21) h21
[PROOF STEP]
by (simp add:Plane_Bet_sameside_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se h21 l21) k21 \<or> Bet_Point (Se l21 k21) h21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
[PROOF STEP]
have P94 : "Bet_Point (Se k1 l1) h11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1

goal (1 subgoal):
 1. Bet_Point (Se k1 l1) h11
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se k1 l1) h11

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11
[PROOF STEP]
have P95 : "Bet_Point (Se l1 k1) h11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P42
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)
[PROOF STEP]
have P96 : "Eq (Geos (Seg (Se k1 l1)) add Emp) (Geos (Seg (Se k21 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se k1 l1)) add Emp) (Geos (Seg (Se k21 l21)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se k1 l1)) add Emp) (Geos (Seg (Se k21 l21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se k1 l1)) add Emp) (Geos (Seg (Se k21 l21)) add Emp)
[PROOF STEP]
have P97 : "Eq (Geos (Seg (Se l1 k1)) add Emp) (Geos (Seg (Se l21 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se k1 l1)) add Emp) (Geos (Seg (Se k21 l21)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se l1 k1)) add Emp) (Geos (Seg (Se l21 k21)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se l1 k1)) add Emp) (Geos (Seg (Se l21 k21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P38
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr o1 h11 l1)) add Emp) (Geos (Tri (Tr o2 h21 l21)) add Emp)
[PROOF STEP]
have "Eq (Geos (Seg (Se h11 l1)) add Emp) (Geos (Seg (Se h21 l21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr o1 h11 l1)) add Emp) (Geos (Tri (Tr o2 h21 l21)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se h11 l1)) add Emp) (Geos (Seg (Se h21 l21)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se h11 l1)) add Emp) (Geos (Seg (Se h21 l21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se h11 l1)) add Emp) (Geos (Seg (Se h21 l21)) add Emp)
[PROOF STEP]
have P98 : "Eq (Geos (Seg (Se l1 h11)) add Emp) (Geos (Seg (Se l21 h21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se h11 l1)) add Emp) (Geos (Seg (Se h21 l21)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se l1 h11)) add Emp) (Geos (Seg (Se l21 h21)) add Emp)
[PROOF STEP]
by (blast intro:Eq_rev Eq_trans Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se l1 h11)) add Emp) (Geos (Seg (Se l21 h21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P95 P97 P98
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se l1 k1) h11
Eq (Geos (Seg (Se l1 k1)) add Emp) (Geos (Seg (Se l21 k21)) add Emp)
Eq (Geos (Seg (Se l1 h11)) add Emp) (Geos (Seg (Se l21 h21)) add Emp)
[PROOF STEP]
have P99 : "\<not> Bet_Point (Se l21 h21) k21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se l1 k1) h11
Eq (Geos (Seg (Se l1 k1)) add Emp) (Geos (Seg (Se l21 k21)) add Emp)
Eq (Geos (Seg (Se l1 h11)) add Emp) (Geos (Seg (Se l21 h21)) add Emp)

goal (1 subgoal):
 1. \<not> Bet_Point (Se l21 h21) k21
[PROOF STEP]
by (blast intro:Seg_Bet_wrong_relation)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se l21 h21) k21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se l21 h21) k21
[PROOF STEP]
have P100 : "\<not> Bet_Point (Se h21 l21) k21"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se l21 h21) k21

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P93 P100
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h21 l21) k21 \<or> Bet_Point (Se l21 k21) h21
\<not> Bet_Point (Se h21 l21) k21
[PROOF STEP]
have "Bet_Point (Se l21 k21) h21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h21 l21) k21 \<or> Bet_Point (Se l21 k21) h21
\<not> Bet_Point (Se h21 l21) k21

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se l21 k21) h21
[PROOF STEP]
have P101 : "\<not> Seg_on_Seg (Se k21 h21) (Se h21 l21)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se l21 k21) h21

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se k21 h21) (Se h21 l21)
[PROOF STEP]
by (simp add:Bet_rev Seg_Bet_not_on)
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se k21 h21) (Se h21 l21)

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P94
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11
[PROOF STEP]
have P104 : "Line_on (Li k1 l1) h11"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11

goal (1 subgoal):
 1. Line_on (Li k1 l1) h11
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li k1 l1) h11

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P94
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11
[PROOF STEP]
have P105 : "\<not> Seg_on_Seg (Se k1 h11) (Se h11 l1)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11

goal (1 subgoal):
 1. \<not> Seg_on_Seg (Se k1 h11) (Se h11 l1)
[PROOF STEP]
by (simp add:Seg_Bet_not_on)
[PROOF STATE]
proof (state)
this:
\<not> Seg_on_Seg (Se k1 h11) (Se h11 l1)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P84 P85 P86 P96 P101 P102 P103 P104 P105
[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)
Ang_inside (An k1 o1 l1) h1
Line_on (Li k21 l21) h21
Line_on (Li k21 l21) k21
Line_on (Li k21 l21) l21
Eq (Geos (Seg (Se k1 l1)) add Emp) (Geos (Seg (Se k21 l21)) add Emp)
\<not> Seg_on_Seg (Se k21 h21) (Se h21 l21)
Line_on (Li k1 l1) k1
Line_on (Li k1 l1) l1
Line_on (Li k1 l1) h11
\<not> Seg_on_Seg (Se k1 h11) (Se h11 l1)
[PROOF STEP]
have P106 : "Eq (Geos (Seg (Se k1 h11)) add Emp) (Geos (Seg (Se k21 h21)) 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)
Ang_inside (An k1 o1 l1) h1
Line_on (Li k21 l21) h21
Line_on (Li k21 l21) k21
Line_on (Li k21 l21) l21
Eq (Geos (Seg (Se k1 l1)) add Emp) (Geos (Seg (Se k21 l21)) add Emp)
\<not> Seg_on_Seg (Se k21 h21) (Se h21 l21)
Line_on (Li k1 l1) k1
Line_on (Li k1 l1) l1
Line_on (Li k1 l1) h11
\<not> Seg_on_Seg (Se k1 h11) (Se h11 l1)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se k1 h11)) add Emp) (Geos (Seg (Se k21 h21)) add Emp)
[PROOF STEP]
by (simp add:Seg_sub)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se k1 h11)) add Emp) (Geos (Seg (Se k21 h21)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P42
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)
[PROOF STEP]
have P107 : "Cong (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An l21 k21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr o1 k1 l1)) add Emp) (Geos (Tri (Tr o2 k21 l21)) add Emp)

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P94
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11
[PROOF STEP]
have "Inv (Bet_Point (Se l1 h11) k1)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11

goal (1 subgoal):
 1. Inv (Bet_Point (Se l1 h11) k1)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se l1 h11) k1)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se l1 h11) k1)
[PROOF STEP]
have P109 : "\<not> Bet_Point (Se l1 h11) k1"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se l1 h11) k1)

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P111 : "\<not> Bet_Point (Se o1 o1) k1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se o1 o1) k1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se o1 o1) k1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P94
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11
[PROOF STEP]
have "\<not> Eq (Geos (Poi h11) add Emp) (Geos (Poi k1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi h11) add Emp) (Geos (Poi k1) add Emp)
[PROOF STEP]
have P112 : "\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi h11) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi h11) add Emp) (Geos (Poi k1) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P108
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An l1 k1 o1))
[PROOF STEP]
have P113 : "\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An l1 k1 o1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P104 P108 P109 P110 P111 P112 P113
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li k1 l1) h11
Def (Ang (An l1 k1 o1))
\<not> Bet_Point (Se l1 h11) k1
Line_on (Li k1 o1) o1
\<not> Bet_Point (Se o1 o1) k1
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi h11) add Emp)
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)
[PROOF STEP]
have P114 : "Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li k1 l1) h11
Def (Ang (An l1 k1 o1))
\<not> Bet_Point (Se l1 h11) k1
Line_on (Li k1 o1) o1
\<not> Bet_Point (Se o1 o1) k1
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi h11) add Emp)
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
[PROOF STEP]
have P115 : "Def (Ang (An l21 k21 o2))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P117 : "\<not> Bet_Point (Se o2 o2) k21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se o2 o2) k21
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se o2 o2) k21

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P64
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
[PROOF STEP]
have P119 : "\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi o2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from assms P71 P84 P99 P115 P116 P117 P119
[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)
Ang_inside (An k1 o1 l1) h1
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
Line_on (Li k21 l21) h21
\<not> Bet_Point (Se l21 h21) k21
Def (Ang (An l21 k21 o2))
Line_on (Li k21 o2) o2
\<not> Bet_Point (Se o2 o2) k21
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi o2) add Emp)
[PROOF STEP]
have P120 : "Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))"
[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)
Ang_inside (An k1 o1 l1) h1
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi h21) add Emp)
Line_on (Li k21 l21) h21
\<not> Bet_Point (Se l21 h21) k21
Def (Ang (An l21 k21 o2))
Line_on (Li k21 o2) o2
\<not> Bet_Point (Se o2 o2) k21
\<not> Eq (Geos (Poi k21) add Emp) (Geos (Poi o2) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P107 P114
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An l21 k21 o2)) add Emp)
Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))
[PROOF STEP]
have P121 : "Cong (Geos (Ang (An h11 k1 o1)) add Emp) (Geos (Ang (An l21 k21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An l21 k21 o2)) add Emp)
Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P120 P121
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))
Cong (Geos (Ang (An h11 k1 o1)) add Emp) (Geos (Ang (An l21 k21 o2)) add Emp)
[PROOF STEP]
have P122 : " Cong (Geos (Ang (An h11 k1 o1)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))
Cong (Geos (Ang (An h11 k1 o1)) add Emp) (Geos (Ang (An l21 k21 o2)) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P114
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))
[PROOF STEP]
have P123 : "Def (Tri (Tr k1 h11 o1))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P120
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))
[PROOF STEP]
have P124 : "Def (Tri (Tr k21 h21 o2))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
[PROOF STEP]
have P125 : "Eq (Geos (Seg (Se k1 o1)) add Emp) (Geos (Seg (Se k21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))

goal (1 subgoal):
 1. Eq (Geos (Seg (Se k1 o1)) add Emp) (Geos (Seg (Se k21 o2)) add Emp)
[PROOF STEP]
by (blast intro:Seg_rev Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se k1 o1)) add Emp) (Geos (Seg (Se k21 o2)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P106 P122 P123 P124 P125
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se k1 h11)) add Emp) (Geos (Seg (Se k21 h21)) add Emp)
Cong (Geos (Ang (An h11 k1 o1)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp)
Def (Tri (Tr k1 h11 o1))
Def (Tri (Tr k21 h21 o2))
Eq (Geos (Seg (Se k1 o1)) add Emp) (Geos (Seg (Se k21 o2)) add Emp)
[PROOF STEP]
have "Cong (Geos (Tri (Tr k1 h11 o1)) add Emp) (Geos (Tri (Tr k21 h21 o2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se k1 h11)) add Emp) (Geos (Seg (Se k21 h21)) add Emp)
Cong (Geos (Ang (An h11 k1 o1)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp)
Def (Tri (Tr k1 h11 o1))
Def (Tri (Tr k21 h21 o2))
Eq (Geos (Seg (Se k1 o1)) add Emp) (Geos (Seg (Se k21 o2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr k1 h11 o1)) add Emp) (Geos (Tri (Tr k21 h21 o2)) add Emp)
[PROOF STEP]
by (simp add:Tri_SAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr k1 h11 o1)) add Emp) (Geos (Tri (Tr k21 h21 o2)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr k1 h11 o1)) add Emp) (Geos (Tri (Tr k21 h21 o2)) add Emp)
[PROOF STEP]
have P126 : "Cong (Geos (Ang (An k1 o1 h11)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr k1 h11 o1)) add Emp) (Geos (Tri (Tr k21 h21 o2)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An k1 o1 h11)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An k1 o1 h11)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P126 P127
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 h11)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)
Eq (Geos (Ang (An k1 o1 h11)) add Emp) (Geos (Ang (An h11 o1 k1)) add Emp)
[PROOF STEP]
have P129 : "Cong (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 h11)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)
Eq (Geos (Ang (An k1 o1 h11)) add Emp) (Geos (Ang (An h11 o1 k1)) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P128 P129
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An k21 o2 h21)) add Emp) (Geos (Ang (An h21 o2 k21)) add Emp)
Cong (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)
[PROOF STEP]
have P130 : "Cong (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h21 o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An k21 o2 h21)) add Emp) (Geos (Ang (An h21 o2 k21)) add Emp)
Cong (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An k21 o2 h21)) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P114
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))
[PROOF STEP]
have P131 : "Def (Ang (An h11 o1 k1))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An l1 k1 o1)) add Emp) (Geos (Ang (An h11 k1 o1)) add Emp) \<and> Def (Ang (An h11 k1 o1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h1 o1 l1))
[PROOF STEP]
have "\<not> Eq (Geos (Poi h1) add Emp) (Geos (Poi o1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h1 o1 l1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi h1) add Emp) (Geos (Poi o1) add Emp)
[PROOF STEP]
have P132 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi h1) add Emp) (Geos (Poi o1) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P10 P12 P132
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h11) add Emp)
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
[PROOF STEP]
have P133 : "Line_on (Li o1 h11) h1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se k1 l1) h11 \<and> Line_on (Li o1 h1) h11 \<and> \<not> Line_on (Li o1 h1) k1 \<and> \<not> Line_on (Li o1 h1) l1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h11) add Emp)
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)

goal (1 subgoal):
 1. Line_on (Li o1 h11) h1
[PROOF STEP]
by (blast intro:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li o1 h11) h1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P27
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se h1 h11) o1
[PROOF STEP]
have P134 : "\<not> Bet_Point (Se h11 h1) o1"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se h1 h11) o1

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P135 : "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 (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
have P136 : "\<not> Bet_Point (Se k1 k1) o1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se k1 k1) o1
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se k1 k1) o1

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An k1 o1 l1))
[PROOF STEP]
have "\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An k1 o1 l1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)
[PROOF STEP]
have P137 : "\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k1) add Emp) (Geos (Poi o1) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P131 P132 P133 P134 P135 P136 P137
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An h11 o1 k1))
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
Line_on (Li o1 h11) h1
\<not> Bet_Point (Se h11 h1) o1
Line_on (Li o1 k1) k1
\<not> Bet_Point (Se k1 k1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)
[PROOF STEP]
have P138 : "Eq (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp) \<and> Def (Ang (An h1 o1 k1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An h11 o1 k1))
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi h1) add Emp)
Line_on (Li o1 h11) h1
\<not> Bet_Point (Se h11 h1) o1
Line_on (Li o1 k1) k1
\<not> Bet_Point (Se k1 k1) o1
\<not> Eq (Geos (Poi o1) add Emp) (Geos (Poi k1) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp) \<and> Def (Ang (An h1 o1 k1))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp) \<and> Def (Ang (An h1 o1 k1))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P120
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))
[PROOF STEP]
have P139 : "Def (Ang (An h21 o2 k21))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An l21 k21 o2)) add Emp) (Geos (Ang (An h21 k21 o2)) add Emp) \<and> Def (Ang (An h21 k21 o2))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P15 P16
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
have P140 : "Line_on (Li o2 h21) h2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)

goal (1 subgoal):
 1. Line_on (Li o2 h21) h2
[PROOF STEP]
by (simp add:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 h21) h2

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
have P141 : "\<not> Bet_Point (Se h21 h2) o2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)

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

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

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi o2) add Emp)
[PROOF STEP]
have P142 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi k2) add Emp) (Geos (Poi o2) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9 P64 P142
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
[PROOF STEP]
have P143 : "Line_on (Li o2 k21) k2"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9 P15 P139 P140 P141 P142 P143
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Def (Ang (An h21 o2 k21))
Line_on (Li o2 h21) h2
\<not> Bet_Point (Se h21 h2) o2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Line_on (Li o2 k21) k2
[PROOF STEP]
have P143 : "Eq (Geos (Ang (An h21 o2 k21)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp) \<and> Def (Ang (An h2 o2 k2))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Def (Ang (An h21 o2 k21))
Line_on (Li o2 h21) h2
\<not> Bet_Point (Se h21 h2) o2
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Line_on (Li o2 k21) k2

goal (1 subgoal):
 1. Eq (Geos (Ang (An h21 o2 k21)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp) \<and> Def (Ang (An h2 o2 k2))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An h21 o2 k21)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp) \<and> Def (Ang (An h2 o2 k2))

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P130 P138
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h21 o2 k21)) add Emp)
Eq (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp) \<and> Def (Ang (An h1 o1 k1))
[PROOF STEP]
have P145 : "Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h21 o2 k21)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h21 o2 k21)) add Emp)
Eq (Geos (Ang (An h11 o1 k1)) add Emp) (Geos (Ang (An h1 o1 k1)) add Emp) \<and> Def (Ang (An h1 o1 k1))

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)
 2. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P143 P145
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An h21 o2 k21)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp) \<and> Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h21 o2 k21)) 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:
Eq (Geos (Ang (An h21 o2 k21)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp) \<and> Def (Ang (An h2 o2 k2))
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h21 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]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An h1 o1 k1)) add Emp) (Geos (Ang (An h2 o2 k2)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P93 P100
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se h21 l21) k21 \<or> Bet_Point (Se l21 k21) h21
\<not> Bet_Point (Se h21 l21) k21
[PROOF STEP]
have P146 : "Bet_Point (Se k21 l21) h21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se h21 l21) k21 \<or> Bet_Point (Se l21 k21) h21
\<not> Bet_Point (Se h21 l21) k21

goal (1 subgoal):
 1. Bet_Point (Se k21 l21) h21
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se k21 l21) h21

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

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

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P30 P64 P146 P147
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
Bet_Point (Se k21 l21) h21
\<not> Eq (Geos (Lin (Li o2 k21)) add Emp) (Geos (Lin (Li o2 l21)) add Emp)
[PROOF STEP]
have P148 : "Ang_inside (An k21 o2 l21) h21"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l21) add Emp)
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k21) add Emp)
Bet_Point (Se k21 l21) h21
\<not> Eq (Geos (Lin (Li o2 k21)) add Emp) (Geos (Lin (Li o2 l21)) add Emp)

goal (1 subgoal):
 1. Ang_inside (An k21 o2 l21) h21
[PROOF STEP]
by (simp add:Ang_inside_Bet_Point)
[PROOF STATE]
proof (state)
this:
Ang_inside (An k21 o2 l21) h21

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An k2 o2 l2))
[PROOF STEP]
have P149 : "\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An k2 o2 l2))

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

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P9 P142 P148 P149
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Ang_inside (An k21 o2 l21) h21
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)
[PROOF STEP]
have P150 : "Ang_inside (An k2 o2 l2) h21"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An k1 o1 l1)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Ang (An k2 o2 l2)) add Emp) (Geos (Ang (An k21 o2 l21)) add Emp) \<and> Eq (Geos (Seg (Se o1 k1)) add Emp) (Geos (Seg (Se o2 k21)) add Emp) \<and> Line_on (Li o2 k2) k21 \<and> \<not> Bet_Point (Se k21 k2) o2 \<and> Eq (Geos (Seg (Se o1 l1)) add Emp) (Geos (Seg (Se o2 l21)) add Emp) \<and> Line_on (Li o2 l2) l21 \<and> \<not> Bet_Point (Se l21 l2) o2 \<and> Def (Ang (An k21 o2 l21))
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi k2) add Emp)
Ang_inside (An k21 o2 l21) h21
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi l2) add Emp)

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h21
[PROOF STEP]
by (simp add:Ang_inside_trans)
[PROOF STATE]
proof (state)
this:
Ang_inside (An k2 o2 l2) h21

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P15 P16
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
have P151 : "Line_on (Li o2 h21) h2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)

goal (1 subgoal):
 1. Line_on (Li o2 h21) h2
[PROOF STEP]
by (simp add:Line_on_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li o2 h21) h2

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)
[PROOF STEP]
have P152 : "\<not> Bet_Point (Se h2 h21) o2"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se o1 h11)) add Emp) (Geos (Seg (Se o2 h21)) add Emp) \<and> \<not> Bet_Point (Se h21 h2) o2 \<and> Line_on (Li o2 h2) h21 \<and> \<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h21) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
from P15 P150 P151 P152
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Ang_inside (An k2 o2 l2) h21
Line_on (Li o2 h21) h2
\<not> Bet_Point (Se h2 h21) o2
[PROOF STEP]
show "Ang_inside (An k2 o2 l2) h2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi o2) add Emp) (Geos (Poi h2) add Emp)
Ang_inside (An k2 o2 l2) h21
Line_on (Li o2 h21) h2
\<not> Bet_Point (Se h2 h21) o2

goal (1 subgoal):
 1. Ang_inside (An k2 o2 l2) h2
[PROOF STEP]
by (simp add:Ang_inside_HalfLine)
[PROOF STATE]
proof (state)
this:
Ang_inside (An k2 o2 l2) h2

goal:
No subgoals!
[PROOF STEP]
qed