[STATEMENT]
theorem (in Congruence_Rule) Seg_bisection :
  assumes
    "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
  shows
    "\<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have "\<exists>p q r. \<not> Line_on (Li A B) p \<and> \<not> Line_on (Li A B) q \<and> \<not> Line_on (Li A B) r
    \<and> \<not> Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) \<and> \<not> Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp)
    \<and> \<not> Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p q r. \<not> Line_on (Li A B) p \<and> \<not> Line_on (Li A B) q \<and> \<not> Line_on (Li A B) r \<and> \<not> Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) \<and> \<not> Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp) \<and> \<not> Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by (blast intro:Line_not_on_exist)
[PROOF STATE]
proof (state)
this:
\<exists>p q r. \<not> Line_on (Li A B) p \<and> \<not> Line_on (Li A B) q \<and> \<not> Line_on (Li A B) r \<and> \<not> Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) \<and> \<not> Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp) \<and> \<not> Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p q r. \<not> Line_on (Li A B) p \<and> \<not> Line_on (Li A B) q \<and> \<not> Line_on (Li A B) r \<and> \<not> Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) \<and> \<not> Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp) \<and> \<not> Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain C :: Point where P1 : "\<not> Line_on (Li A B) C"
[PROOF STATE]
proof (prove)
using this:
\<exists>p q r. \<not> Line_on (Li A B) p \<and> \<not> Line_on (Li A B) q \<and> \<not> Line_on (Li A B) r \<and> \<not> Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) \<and> \<not> Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp) \<and> \<not> Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>C. \<not> Line_on (Li A B) C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C
[PROOF STEP]
have P2 : "Def (Ang (An A B C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Line_on (Li A B) C

goal (1 subgoal):
 1. Def (Ang (An A B C))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A B C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P2 : "Def (Ang (An C A B))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

goal (1 subgoal):
 1. Def (Ang (An C A B))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An C A B))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P3 : "Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P1 P3
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li A B) C
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P4 : "\<not> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li A B) C
Eq (Geos (Lin (Li A B)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Line_not_on_trans)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B A) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2 P4
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
\<not> Line_on (Li B A) C
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp)
    \<and> Plane_diffside (Li B A) p C"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))
\<not> Line_on (Li B A) C

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Plane_diffside (Li B A) p C
[PROOF STEP]
by (simp add:Ang_move_diffside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Plane_diffside (Li B A) p C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Plane_diffside (Li B A) p C
[PROOF STEP]
obtain D1 :: Point where P5 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp)
    \<and> Plane_diffside (Li B A) D1 C"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Plane_diffside (Li B A) p C

goal (1 subgoal):
 1. (\<And>D1. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C
[PROOF STEP]
have "\<exists>p. Bet_Point (Se D1 C) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D1 \<and> \<not> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se D1 C) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D1 \<and> \<not> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se D1 C) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D1 \<and> \<not> Line_on (Li B A) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se D1 C) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D1 \<and> \<not> Line_on (Li B A) C
[PROOF STEP]
have P6 : "\<not> Line_on (Li B A) D1"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se D1 C) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D1 \<and> \<not> Line_on (Li B A) C

goal (1 subgoal):
 1. \<not> Line_on (Li B A) D1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B A) D1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P6 P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) D1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have "Def (Ang (An B A D1))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) D1
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)

goal (1 subgoal):
 1. Def (Ang (An B A D1))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B A D1))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B A D1))
[PROOF STEP]
have P8 : "Def (Ang (An D1 B A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B A D1))

goal (1 subgoal):
 1. Def (Ang (An D1 B A))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An D1 B A))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2 P5 P8
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C
Def (Ang (An D1 B A))
[PROOF STEP]
have "\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp)
    \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An p B A)) add Emp)
    \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B p)) add Emp) \<and> Line_on (Li B D1) p
    \<and> \<not> Bet_Point (Se p D1) B \<and> Def (Ang (An p B A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C
Def (Ang (An D1 B A))

goal (1 subgoal):
 1. \<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B p)) add Emp) \<and> Line_on (Li B D1) p \<and> \<not> Bet_Point (Se p D1) B \<and> Def (Ang (An p B A))
[PROOF STEP]
by (simp add:Ang_replace)
[PROOF STATE]
proof (state)
this:
\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B p)) add Emp) \<and> Line_on (Li B D1) p \<and> \<not> Bet_Point (Se p D1) B \<and> Def (Ang (An p B A))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B p)) add Emp) \<and> Line_on (Li B D1) p \<and> \<not> Bet_Point (Se p D1) B \<and> Def (Ang (An p B A))
[PROOF STEP]
obtain D :: Point where P9 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp)
    \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp)
    \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D
    \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An p B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B p)) add Emp) \<and> Line_on (Li B D1) p \<and> \<not> Bet_Point (Se p D1) B \<and> Def (Ang (An p B A))

goal (1 subgoal):
 1. (\<And>D. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have "Plane_diffside (Li B A) D D1 \<Longrightarrow>
    \<exists>p. Bet_Point (Se D D1) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> \<exists>p. Bet_Point (Se D D1) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<exists>p. Bet_Point (Se D D1) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<exists>p. Bet_Point (Se D D1) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
[PROOF STEP]
obtain B1 :: Point where P10 : "Plane_diffside (Li B A) D D1 \<Longrightarrow>
    Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<exists>p. Bet_Point (Se D D1) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1

goal (1 subgoal):
 1. (\<And>B1. (Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
[PROOF STEP]
have P11 : "Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B1
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P10
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
[PROOF STEP]
have "Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1
[PROOF STEP]
have P12 : "Plane_diffside (Li B A) D D1 \<Longrightarrow>
    \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp)
[PROOF STEP]
by (simp add:Bet_Point_def)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P13 : "Line_on (Li B D1) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D1) D1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D1) D1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P14 : "Line_on (Li D D1) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D D1) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D D1) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P15 : "Line_on (Li D D1) D1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D D1) D1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D D1) D1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
[PROOF STEP]
have P16 : "Line_on (Li B D1) D"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))

goal (1 subgoal):
 1. Line_on (Li B D1) D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on (Li B D1) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P12 P13 P14 P15 P16
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B D1) D1
Line_on (Li D D1) D
Line_on (Li D D1) D1
Line_on (Li B D1) D
[PROOF STEP]
have P17 : "Plane_diffside (Li B A) D D1 \<Longrightarrow>
    Eq (Geos (Lin (Li B D1)) add Emp) (Geos (Lin (Li D D1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi D1) add Emp)
Line_on (Li B D1) D1
Line_on (Li D D1) D
Line_on (Li D D1) D1
Line_on (Li B D1) D

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Lin (Li B D1)) add Emp) (Geos (Lin (Li D D1)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Lin (Li B D1)) add Emp) (Geos (Lin (Li D D1)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P18 : "Line_on (Li B D1) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D1) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D1) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P17 P18
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Lin (Li B D1)) add Emp) (Geos (Lin (Li D D1)) add Emp)
Line_on (Li B D1) B
[PROOF STEP]
have P19 : "Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Lin (Li B D1)) add Emp) (Geos (Lin (Li D D1)) add Emp)
Line_on (Li B D1) B

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P14
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li D D1) D
[PROOF STEP]
have P20 : "Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow>
    Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li D D1) D

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P10 P20
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P21 : "Plane_diffside (Li B A) D D1 \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) D

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P22 : "Line_on (Li B A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P10 P11 P19 P21 P22
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B1
Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp)
Line_on (Li B A) B
[PROOF STEP]
have P23 : "Plane_diffside (Li B A) D D1 \<Longrightarrow>
    Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B1
Plane_diffside (Li B A) D D1 \<Longrightarrow> Line_on (Li D D1) B
Plane_diffside (Li B A) D D1 \<Longrightarrow> \<not> Eq (Geos (Lin (Li D D1)) add Emp) (Geos (Lin (Li B A)) add Emp)
Line_on (Li B A) B

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
by (simp add:Line_unique_Point)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P10 P23
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P24 : "Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) D \<and> \<not> Line_on (Li B A) D1
Plane_diffside (Li B A) D D1 \<Longrightarrow> Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B
[PROOF STEP]
by (blast intro:Point_Eq)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P24
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B
[PROOF STEP]
have P25 : "\<not> Plane_diffside (Li B A) D D1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Plane_diffside (Li B A) D D1 \<Longrightarrow> Bet_Point (Se D D1) B

goal (1 subgoal):
 1. \<not> Plane_diffside (Li B A) D D1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Plane_diffside (Li B A) D D1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C
[PROOF STEP]
have P26 : "Plane_sameside (Li B A) C D \<Longrightarrow> Plane_diffside (Li B A) D D1"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C

goal (1 subgoal):
 1. Plane_sameside (Li B A) C D \<Longrightarrow> Plane_diffside (Li B A) D D1
[PROOF STEP]
by (simp add:Plane_diffside_rev Plane_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li B A) C D \<Longrightarrow> Plane_diffside (Li B A) D D1

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P25 P26
[PROOF STATE]
proof (chain)
picking this:
\<not> Plane_diffside (Li B A) D D1
Plane_sameside (Li B A) C D \<Longrightarrow> Plane_diffside (Li B A) D D1
[PROOF STEP]
have P27 : "\<not> Plane_sameside (Li B A) C D"
[PROOF STATE]
proof (prove)
using this:
\<not> Plane_diffside (Li B A) D D1
Plane_sameside (Li B A) C D \<Longrightarrow> Plane_diffside (Li B A) D D1

goal (1 subgoal):
 1. \<not> Plane_sameside (Li B A) C D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Plane_sameside (Li B A) C D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C
[PROOF STEP]
have P28 : "Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow>
    Plane_diffside (Li B A) D1 D"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D1 B A)) add Emp) \<and> Plane_diffside (Li B A) D1 C

goal (1 subgoal):
 1. Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Plane_diffside (Li B A) D1 D
[PROOF STEP]
by (blast intro:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Plane_diffside (Li B A) D1 D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P25 P28
[PROOF STATE]
proof (chain)
picking this:
\<not> Plane_diffside (Li B A) D D1
Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Plane_diffside (Li B A) D1 D
[PROOF STEP]
have P29 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Plane_diffside (Li B A) D D1
Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Plane_diffside (Li B A) D1 D

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
[PROOF STEP]
have "Def (Tri (Tr B A D))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B A D))
[PROOF STEP]
have P30 : "\<not> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B A D))

goal (1 subgoal):
 1. \<not> Line_on (Li B A) D
[PROOF STEP]
by (simp add:Tri_def_Line)
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B A) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P4 P27 P29 P30
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) C
\<not> Plane_sameside (Li B A) C D
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp)
\<not> Line_on (Li B A) D
[PROOF STEP]
have "Plane_diffside (Li B A) C D"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) C
\<not> Plane_sameside (Li B A) C D
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp)
\<not> Line_on (Li B A) D

goal (1 subgoal):
 1. Plane_diffside (Li B A) C D
[PROOF STEP]
by (simp add:Plane_not_sameside_diffside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) C D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) C D
[PROOF STEP]
have "\<exists>p. Bet_Point (Se C D) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) C D

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se C D) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se C D) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se C D) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
[PROOF STEP]
obtain E :: Point where P31 : "Bet_Point (Se C D) E \<and> Line_on (Li B A) E
    \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se C D) p \<and> Line_on (Li B A) p \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D

goal (1 subgoal):
 1. (\<And>E. Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
[PROOF STEP]
have P32 : "Bet_Point (Se C D) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D

goal (1 subgoal):
 1. Bet_Point (Se C D) E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se C D) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E
[PROOF STEP]
have P33 : "Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Bet_Point (Se D C) A"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E

goal (1 subgoal):
 1. Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Bet_Point (Se D C) A
[PROOF STEP]
by (blast intro:Point_Eq Bet_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Bet_Point (Se D C) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
[PROOF STEP]
have P34 : "Def (Tri (Tr A D B))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P33 P34
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Bet_Point (Se D C) A
Def (Tri (Tr A D B))
[PROOF STEP]
have P35 : "Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow>
    Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Bet_Point (Se D C) A
Def (Tri (Tr A D B))

goal (1 subgoal):
 1. Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P32
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E
[PROOF STEP]
have P36 : "Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Bet_Point (Se C D) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E

goal (1 subgoal):
 1. Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Bet_Point (Se C D) B
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Bet_Point (Se C D) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
[PROOF STEP]
have P37 : "Def (Tri (Tr B C A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P36 P37
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Bet_Point (Se C D) B
Def (Tri (Tr B C A))
[PROOF STEP]
have P38 : "Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow>
    Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Bet_Point (Se C D) B
Def (Tri (Tr B C A))

goal (1 subgoal):
 1. Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P39 : "Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P39
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
have P40 : "Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D B A)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D B A)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P41 : "Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P40 P41
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
have P42 : "Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
[PROOF STEP]
have P43 : "Def (Ang (An B A C))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))

goal (1 subgoal):
 1. Def (Ang (An B A C))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B A C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
[PROOF STEP]
have P44 : "Def (Ang (An A B D))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))

goal (1 subgoal):
 1. Def (Ang (An A B D))
[PROOF STEP]
by (simp add:Ang_def_rev)
[PROOF STATE]
proof (state)
this:
Def (Ang (An A B D))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P42 P43 P44
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)
Def (Ang (An B A C))
Def (Ang (An A B D))
[PROOF STEP]
have P45 : "\<not> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)
Def (Ang (An B A C))
Def (Ang (An A B D))

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Gr)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P35 P45
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)
\<not> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
have P46 : "\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp)
\<not> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P38 P45
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)
\<not> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
have P47 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)
\<not> Gr (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An B A C)) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P48 : "Line_on (Li B A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P49 : "Line_on (Li B A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P31 P46 P47 P48 P49
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
[PROOF STEP]
have P50 : "Bet_Point (Se A E) B \<or> Bet_Point (Se E B) A
    \<or> Bet_Point (Se B A) E"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<or> Bet_Point (Se E B) A \<or> Bet_Point (Se B A) E
[PROOF STEP]
by (simp add:Bet_case)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<or> Bet_Point (Se E B) A \<or> Bet_Point (Se B A) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P51 : "Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li B E) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li B E) A
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li B E) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P52 : "Line_on (Li B E) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B E) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B E) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P48 P49 P51 P52
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li B E) A
Line_on (Li B E) B
[PROOF STEP]
have "Bet_Point (Se A E) B \<Longrightarrow>
    Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li B E) A
Line_on (Li B E) B

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P53 : "Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li B E) D \<Longrightarrow> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se A E) B; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P30 P53
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P54 : "Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li B E) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li B E) D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li B E) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P47 P54
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li B E) D
[PROOF STEP]
have P55 : "Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr B E D))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li B E) D

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr B E D))
[PROOF STEP]
by (simp add:Ang_sinple_def Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr B E D))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P56 : "Bet_Point (Se A E) B \<Longrightarrow> Bet_Point (Se E A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Bet_Point (Se E A) B
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Bet_Point (Se E A) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P55 P56
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr B E D))
Bet_Point (Se A E) B \<Longrightarrow> Bet_Point (Se E A) B
[PROOF STEP]
have P57 : "Bet_Point (Se A E) B \<Longrightarrow>
    Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B E D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr B E D))
Bet_Point (Se A E) B \<Longrightarrow> Bet_Point (Se E A) B

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B E D)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B E D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P58 : "Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) B
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P59 : "Line_on (Li E A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li E A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li E A) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P48 P49 P58 P59
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) B
Line_on (Li E A) A
[PROOF STEP]
have P60 : "Bet_Point (Se A E) B \<Longrightarrow>
    Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) B
Line_on (Li E A) A

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P61 : "Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) C \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P31 P61
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P62 : "Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) C"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P46 P62
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) C
[PROOF STEP]
have "Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E A C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) C

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E A C))
[PROOF STEP]
by (simp add:Ang_sinple_def Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E A C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E A C))
[PROOF STEP]
have P63 : "Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E C A))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E A C))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E C A))
[PROOF STEP]
by (blast intro:Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E C A))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P31 P63
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E C A))
[PROOF STEP]
have P64 : "Bet_Point (Se A E) B \<Longrightarrow>
    Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An E A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E C A))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An E A C)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An E A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P63
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E C A))
[PROOF STEP]
have P65 : "Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A C))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Tri (Tr E C A))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A C))
[PROOF STEP]
by (blast intro:Tri_to_Ang Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P66 : "Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li A E) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li A E) B
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li A E) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have "Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se E B) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se E B) A)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se E B) A)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se E B) A)
[PROOF STEP]
have P67 : "Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se E B) A"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se E B) A)

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se E B) A
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se E B) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P68 : "Line_on (Li A C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P69 : "\<not> Bet_Point (Se C C) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C C) A
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C C) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
[PROOF STEP]
have "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P70 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P65 P66 P67 P68 P69 P70
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A C))
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li A E) B
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se E B) A
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P71 : "Bet_Point (Se A E) B \<Longrightarrow>
    Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A C))
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li A E) B
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se E B) A
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))
[PROOF STEP]
have P72 : "Bet_Point (Se A E) B \<Longrightarrow>
    Cong (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P60
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P73 : "Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) D \<Longrightarrow> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P31 P73
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P74 : "Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) D"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se A E) B; Line_on (Li E A) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P46 P74
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) D
[PROOF STEP]
have "Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A D))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Line_on (Li E A) D

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A D))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A D))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A D))
[PROOF STEP]
have P75 : "Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A D))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P64 P65 P71 P72 P75
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An E A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A C))
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))
Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
[PROOF STEP]
have P76 : "Bet_Point (Se A E) B \<Longrightarrow>
    Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An E A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An E A C))
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))
Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have "Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se B A) E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se B A) E)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se B A) E)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se B A) E)
[PROOF STEP]
have "Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se B A) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Inv (Bet_Point (Se B A) E)

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se B A) E
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se B A) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se B A) E
[PROOF STEP]
have P77 : "Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se A B) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se B A) E

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se A B) E
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se A B) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P78 : "Line_on (Li E D) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li E D) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li E D) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P79 : "\<not> Bet_Point (Se D D) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se D D) E
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se D D) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P47
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
[PROOF STEP]
have P80 : "\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P32
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E
[PROOF STEP]
have "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)
[PROOF STEP]
have P81 : "\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P58 P75 P77 P78 P79 P80 P81
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) B
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se A B) E
Line_on (Li E D) D
\<not> Bet_Point (Se D D) E
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P82 : "Bet_Point (Se A E) B \<Longrightarrow>
    Eq (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp) \<and> Def (Ang (An B E D))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Line_on (Li E A) B
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
Bet_Point (Se A E) B \<Longrightarrow> \<not> Bet_Point (Se A B) E
Line_on (Li E D) D
\<not> Bet_Point (Se D D) E
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp) \<and> Def (Ang (An B E D))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp) \<and> Def (Ang (An B E D))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp) \<and> Def (Ang (An B E D))
[PROOF STEP]
have P83 : "Bet_Point (Se A E) B \<Longrightarrow>
    Cong (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp) \<and> Def (Ang (An B E D))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P57 P75 P82 P83
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B E D)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp) \<and> Def (Ang (An B E D))
Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp)
[PROOF STEP]
have P84 : "Bet_Point (Se A E) B \<Longrightarrow>
    Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A E D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B E D)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp) \<and> Def (Ang (An B E D))
Bet_Point (Se A E) B \<Longrightarrow> Cong (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B E D)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A E D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A E D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P71 P75 P76 P84
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A E D)) add Emp)
[PROOF STEP]
have P85 : "Bet_Point (Se A E) B \<Longrightarrow>
    Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))
Bet_Point (Se A E) B \<Longrightarrow> Def (Ang (An A E D))
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An A E D)) add Emp) (Geos (Ang (An B A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A E D)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Gr)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P40 P71
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))
[PROOF STEP]
have P86 : "Bet_Point (Se A E) B \<Longrightarrow>
    \<not> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Cong (Geos (Ang (An B A C)) add Emp) (Geos (Ang (An D B A)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> Eq (Geos (Ang (An E A C)) add Emp) (Geos (Ang (An B A C)) add Emp) \<and> Def (Ang (An B A C))

goal (1 subgoal):
 1. Bet_Point (Se A E) B \<Longrightarrow> \<not> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Gr)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A E) B \<Longrightarrow> \<not> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P85 P86
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)
[PROOF STEP]
have P87 : "\<not> Bet_Point (Se A E) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<Longrightarrow> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)
Bet_Point (Se A E) B \<Longrightarrow> \<not> Gr (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An B A C)) add Emp)

goal (1 subgoal):
 1. \<not> Bet_Point (Se A E) B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se A E) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P88 : "Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) B
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P48 P49 P59 P88
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Line_on (Li E A) A
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) B
[PROOF STEP]
have P89 : "Bet_Point (Se E B) A \<Longrightarrow>
    Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Line_on (Li E A) A
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) B

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P90 : "Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) C \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se E B) A; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se E B) A; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P31 P90
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se E B) A; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P91 : "Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li E A) C"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se E B) A; Line_on (Li E A) C\<rbrakk> \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li E A) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li E A) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P46 P91
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li E A) C
[PROOF STEP]
have "Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An E A C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li E A) C

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An E A C))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An E A C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An E A C))
[PROOF STEP]
have P92 : "Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr A E C))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An E A C))

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr A E C))
[PROOF STEP]
by (blast intro:Ang_to_Tri Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr A E C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr A E C))
[PROOF STEP]
have P93 : "Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A E C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr A E C))

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A E C)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A E C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P94 : "Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B E) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B E) A
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B E) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P48 P49 P52 P94
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Line_on (Li B E) B
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B E) A
[PROOF STEP]
have "Bet_Point (Se E B) A \<Longrightarrow>
    Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Line_on (Li B E) B
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B E) A

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P95 : "Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B E) D \<Longrightarrow> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Bet_Point (Se E B) A; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Bet_Point (Se E B) A; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P31 P95
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se E B) A; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P96 : "Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li B E) D"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<lbrakk>Bet_Point (Se E B) A; Line_on (Li B E) D\<rbrakk> \<Longrightarrow> Line_on (Li B A) D

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li B E) D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li B E) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P47 P96
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li B E) D
[PROOF STEP]
have "Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An B E D))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> \<not> Line_on (Li B E) D

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An B E D))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An B E D))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An B E D))
[PROOF STEP]
have P97 : "Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr E D B))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An B E D))

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr E D B))
[PROOF STEP]
by (blast intro:Ang_to_Tri Tri_def_rev Tri_def_trans)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr E D B))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P32
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E
[PROOF STEP]
have P98 : "Bet_Point (Se D C) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E

goal (1 subgoal):
 1. Bet_Point (Se D C) E
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D C) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P97 P98
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr E D B))
Bet_Point (Se D C) E
[PROOF STEP]
have P99 : "Bet_Point (Se E B) A \<Longrightarrow>
    Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An E B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr E D B))
Bet_Point (Se D C) E

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An E B D)) add Emp)
[PROOF STEP]
by (simp add:Ang_external_Gr)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An E B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P92
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr A E C))
[PROOF STEP]
have P100 : "Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An A E C))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Tri (Tr A E C))

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An A E C))
[PROOF STEP]
by (simp add:Tri_to_Ang)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An A E C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have "Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se B A) E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se B A) E)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se B A) E)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se B A) E)
[PROOF STEP]
have "Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se B A) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se B A) E)

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se B A) E
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se B A) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se B A) E
[PROOF STEP]
have P101 : "Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A B) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se B A) E

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A B) E
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A B) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P102 : "Line_on (Li E C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li E C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li E C) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P103 : "\<not> Bet_Point (Se C C) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se C C) E
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se C C) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P32
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E
[PROOF STEP]
have P104 : "\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P80 P88 P100 P101 P102 P103 P104
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) B
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An A E C))
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A B) E
Line_on (Li E C) C
\<not> Bet_Point (Se C C) E
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P105 : "Bet_Point (Se E B) A \<Longrightarrow>
    Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li E A) B
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An A E C))
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A B) E
Line_on (Li E C) C
\<not> Bet_Point (Se C C) E
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
[PROOF STEP]
have P106 : "Bet_Point (Se E B) A \<Longrightarrow>
    Cong (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P107 : "Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B A) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B A) E
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B A) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have "Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se A E) B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se A E) B)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se A E) B)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se A E) B)
[PROOF STEP]
have P108 : "Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A E) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Inv (Bet_Point (Se A E) B)

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A E) B
[PROOF STEP]
by (simp add:Inv_def)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A E) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P109 : "Line_on (Li B D) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) D

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P110 : "\<not> Bet_Point (Se D D) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Bet_Point (Se D D) B
[PROOF STEP]
by (simp add:Bet_end_Point)
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se D D) B

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P44
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B D))
[PROOF STEP]
have P111 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B D))

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P44 P47 P107 P108 P109 P110 P111
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B D))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B A) E
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A E) B
Line_on (Li B D) D
\<not> Bet_Point (Se D D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P112 : "Bet_Point (Se E B) A \<Longrightarrow>
    Eq (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp) \<and> Def (Ang (An E B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B D))
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Line_on (Li B A) E
Bet_Point (Se E B) A \<Longrightarrow> \<not> Bet_Point (Se A E) B
Line_on (Li B D) D
\<not> Bet_Point (Se D D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp) \<and> Def (Ang (An E B D))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp) \<and> Def (Ang (An E B D))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp) \<and> Def (Ang (An E B D))
[PROOF STEP]
have P113 : "Bet_Point (Se E B) A \<Longrightarrow>
    Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp) \<and> Def (Ang (An E B D))

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2 P93 P100 P105 P106
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A E C)) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An A E C))
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp)
[PROOF STEP]
have P114 : "Bet_Point (Se E B) A \<Longrightarrow>
    Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B E C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A E C)) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Def (Ang (An A E C))
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B E C)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B E C)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P44 P99 P105 P112 P113
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B D))
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An E B D)) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp) \<and> Def (Ang (An E B D))
Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp)
[PROOF STEP]
have P115 : "Bet_Point (Se E B) A \<Longrightarrow>
    Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B D))
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An E B D)) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp) \<and> Def (Ang (An E B D))
Bet_Point (Se E B) A \<Longrightarrow> Cong (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An E B D)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Eq Ang_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2 P44 P105 P114 P115
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
Def (Ang (An A B D))
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B E C)) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
have P116 : "Bet_Point (Se E B) A \<Longrightarrow>
    Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))
Def (Ang (An A B D))
Bet_Point (Se E B) A \<Longrightarrow> Eq (Geos (Ang (An A E C)) add Emp) (Geos (Ang (An B E C)) add Emp) \<and> Def (Ang (An B E C))
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An B E C)) add Emp)
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An B E C)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_Gr_trans_Gr_Gr)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P41
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
have P117 : "Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2 P44 P117
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
Def (Ang (An A B D))
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)
[PROOF STEP]
have P118 : "\<not> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)
    \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An C A B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))
Def (Ang (An A B D))
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)

goal (1 subgoal):
 1. \<not> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An C A B)) add Emp)
[PROOF STEP]
by (simp add:Ang_not_Gr)
[PROOF STATE]
proof (state)
this:
\<not> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An C A B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P116 P118
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)
\<not> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An C A B)) add Emp)
[PROOF STEP]
have P119 : "\<not> Bet_Point (Se E B) A"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se E B) A \<Longrightarrow> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp)
\<not> Gr (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An A B D)) add Emp) \<and> \<not> Gr (Geos (Ang (An A B D)) add Emp) (Geos (Ang (An C A B)) add Emp)

goal (1 subgoal):
 1. \<not> Bet_Point (Se E B) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se E B) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P50 P87 P119
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se A E) B \<or> Bet_Point (Se E B) A \<or> Bet_Point (Se B A) E
\<not> Bet_Point (Se A E) B
\<not> Bet_Point (Se E B) A
[PROOF STEP]
have P120 : "Bet_Point (Se B A) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se A E) B \<or> Bet_Point (Se E B) A \<or> Bet_Point (Se B A) E
\<not> Bet_Point (Se A E) B
\<not> Bet_Point (Se E B) A

goal (1 subgoal):
 1. Bet_Point (Se B A) E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se B A) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B A) E
[PROOF STEP]
have P121 : "Line_on (Li B E) A"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B A) E

goal (1 subgoal):
 1. Line_on (Li B E) A
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li B E) A

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from assms P48 P49 P52 P121
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Line_on (Li B E) B
Line_on (Li B E) A
[PROOF STEP]
have "Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B A) B
Line_on (Li B A) A
Line_on (Li B E) B
Line_on (Li B E) A

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P122 : "Line_on (Li B E) C \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B E)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. Line_on (Li B E) C \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li B E) C \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P31 P122
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
Line_on (Li B E) C \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P123 : "\<not> Line_on (Li B E) C"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
Line_on (Li B E) C \<Longrightarrow> Line_on (Li B A) C

goal (1 subgoal):
 1. \<not> Line_on (Li B E) C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li B E) C

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P47 P123
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
\<not> Line_on (Li B E) C
[PROOF STEP]
have P124 : "Def (Ang (An B E C))"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
\<not> Line_on (Li B E) C

goal (1 subgoal):
 1. Def (Ang (An B E C))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An B E C))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P32 P120 P124
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E
Bet_Point (Se B A) E
Def (Ang (An B E C))
[PROOF STEP]
have P125 : "Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An B E D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E
Bet_Point (Se B A) E
Def (Ang (An B E C))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An B E D)) add Emp)
[PROOF STEP]
by (simp add:Ang_vertical)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An B E D)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P126 : "Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P127 : "Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se D B)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se D B)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se D B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P126 P127
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se D B)) add Emp)
[PROOF STEP]
have P128 : "Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se D B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se C A)) add Emp)
Eq (Geos (Seg (Se B D)) add Emp) (Geos (Seg (Se D B)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se D B)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se D B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P129 : "Eq (Geos (Ang (An B E D)) add Emp) (Geos (Ang (An D E B)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Ang (An B E D)) add Emp) (Geos (Ang (An D E B)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An B E D)) add Emp) (Geos (Ang (An D E B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P125 P129
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An B E D)) add Emp)
Eq (Geos (Ang (An B E D)) add Emp) (Geos (Ang (An D E B)) add Emp)
[PROOF STEP]
have P130 : "Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An D E B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An B E D)) add Emp)
Eq (Geos (Ang (An B E D)) add Emp) (Geos (Ang (An D E B)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An D E B)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An D E B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P120
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B A) E
[PROOF STEP]
have P131 : "Line_on (Li A B) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B A) E

goal (1 subgoal):
 1. Line_on (Li A B) E
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P119
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se E B) A
[PROOF STEP]
have P132 : "\<not> Bet_Point (Se B E) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se E B) A

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P46
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P133 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)

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

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P2 P68 P69 P70 P131 P132 P133
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C A B))
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Line_on (Li A B) E
\<not> Bet_Point (Se B E) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)
[PROOF STEP]
have P134 :
    "Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A E)) add Emp) \<and> Def (Ang (An C A E))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C A B))
Line_on (Li A C) C
\<not> Bet_Point (Se C C) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Line_on (Li A B) E
\<not> Bet_Point (Se B E) A
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A E)) add Emp) \<and> Def (Ang (An C A E))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A E)) add Emp) \<and> Def (Ang (An C A E))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A E)) add Emp) \<and> Def (Ang (An C A E))
[PROOF STEP]
have P135 : "Def (Tri (Tr C A E))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A E)) add Emp) \<and> Def (Ang (An C A E))

goal (1 subgoal):
 1. Def (Tri (Tr C A E))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr C A E))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9 P134
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A E)) add Emp) \<and> Def (Ang (An C A E))
[PROOF STEP]
have P136 : "Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
Eq (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An C A E)) add Emp) \<and> Def (Ang (An C A E))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B A)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B A)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P9
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))
[PROOF STEP]
have P137 : "Def (Ang (An D B A))"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A B)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Ang (An D1 B A)) add Emp) (Geos (Ang (An D B A)) add Emp) \<and> Eq (Geos (Seg (Se A C)) add Emp) (Geos (Seg (Se B D)) add Emp) \<and> Line_on (Li B D1) D \<and> \<not> Bet_Point (Se D D1) B \<and> Def (Ang (An D B A))

goal (1 subgoal):
 1. Def (Ang (An D B A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Def (Ang (An D B A))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P31 P47 P87 P109 P110 P111 P137
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
\<not> Bet_Point (Se A E) B
Line_on (Li B D) D
\<not> Bet_Point (Se D D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Def (Ang (An D B A))
[PROOF STEP]
have P138 :
    "Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B E)) add Emp) \<and> Def (Ang (An D B E))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C D) E \<and> Line_on (Li B A) E \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
\<not> Bet_Point (Se A E) B
Line_on (Li B D) D
\<not> Bet_Point (Se D D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Def (Ang (An D B A))

goal (1 subgoal):
 1. Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B E)) add Emp) \<and> Def (Ang (An D B E))
[PROOF STEP]
by (simp add:Ang_Point_swap)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B E)) add Emp) \<and> Def (Ang (An D B E))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B E)) add Emp) \<and> Def (Ang (An D B E))
[PROOF STEP]
have P139 : "Def (Tri (Tr D B E))"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B E)) add Emp) \<and> Def (Ang (An D B E))

goal (1 subgoal):
 1. Def (Tri (Tr D B E))
[PROOF STEP]
by (simp add:Ang_to_Tri)
[PROOF STATE]
proof (state)
this:
Def (Tri (Tr D B E))

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P136 P138
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B A)) add Emp)
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B E)) add Emp) \<and> Def (Ang (An D B E))
[PROOF STEP]
have P140 : "Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B A)) add Emp)
Eq (Geos (Ang (An D B A)) add Emp) (Geos (Ang (An D B E)) add Emp) \<and> Def (Ang (An D B E))

goal (1 subgoal):
 1. Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
by (blast intro:Ang_weektrans Ang_rev Eq_rev)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B E)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P128 P130 P135 P139 P140
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se D B)) add Emp)
Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An D E B)) add Emp)
Def (Tri (Tr C A E))
Def (Tri (Tr D B E))
Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
have "Cong (Geos (Tri (Tr C A E)) add Emp) (Geos (Tri (Tr D B E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se C A)) add Emp) (Geos (Seg (Se D B)) add Emp)
Cong (Geos (Ang (An C E A)) add Emp) (Geos (Ang (An D E B)) add Emp)
Def (Tri (Tr C A E))
Def (Tri (Tr D B E))
Cong (Geos (Ang (An C A E)) add Emp) (Geos (Ang (An D B E)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Tri (Tr C A E)) add Emp) (Geos (Tri (Tr D B E)) add Emp)
[PROOF STEP]
by (simp add:Tri_AAS)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Tri (Tr C A E)) add Emp) (Geos (Tri (Tr D B E)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Tri (Tr C A E)) add Emp) (Geos (Tri (Tr D B E)) add Emp)
[PROOF STEP]
have P141 : "Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se B E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Tri (Tr C A E)) add Emp) (Geos (Tri (Tr D B E)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se B E)) add Emp)
[PROOF STEP]
by (simp add:Tri_Cong_def)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se B E)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
have P142 : "Eq (Geos (Seg (Se B E)) add Emp) (Geos (Seg (Se E B)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Seg (Se B E)) add Emp) (Geos (Seg (Se E B)) add Emp)
[PROOF STEP]
by (simp add:Seg_rev)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se B E)) add Emp) (Geos (Seg (Se E B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P141 P142
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se B E)) add Emp)
Eq (Geos (Seg (Se B E)) add Emp) (Geos (Seg (Se E B)) add Emp)
[PROOF STEP]
have P143 : "Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se E B)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se B E)) add Emp)
Eq (Geos (Seg (Se B E)) add Emp) (Geos (Seg (Se E B)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se E B)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se E B)) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P120
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se B A) E
[PROOF STEP]
have P144 : "Bet_Point (Se A B) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se B A) E

goal (1 subgoal):
 1. Bet_Point (Se A B) E
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se A B) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
from P143 P144
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se E B)) add Emp)
Bet_Point (Se A B) E
[PROOF STEP]
show "\<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se A E)) add Emp) (Geos (Seg (Se E B)) add Emp)
Bet_Point (Se A B) E

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se A p)) add Emp) (Geos (Seg (Se p B)) add Emp) \<and> Bet_Point (Se A B) p

goal:
No subgoals!
[PROOF STEP]
qed