[STATEMENT]
theorem (in Congruence_Rule) Ang_vertical :
  assumes
    "Def (Ang (An A B C))"
    "Bet_Point (Se A D) B"
    "Bet_Point (Se C E) B"
  shows "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)"
    and "Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An A B E)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp) &&& Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An A B E)) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
 2. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An A B E)) add Emp)
[PROOF STEP]
have P1 : "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An C B A)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An C B A)) add Emp)
[PROOF STEP]
by (simp add:Ang_roll)
[PROOF STATE]
proof (state)
this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An C B A)) add Emp)

goal (2 subgoals):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
 2. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An A B E)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B
[PROOF STEP]
have P2 : "Def (Ang (An C B A))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B

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

goal (2 subgoals):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
 2. Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An A B E)) add Emp)
[PROOF STEP]
from assms P1 P2
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An C B A)) add Emp)
Def (Ang (An C B A))
[PROOF STEP]
show "Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An A B E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An C B A)) add Emp)
Def (Ang (An C B A))

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B
[PROOF STEP]
have P3 : "Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B

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

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P4 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
from P2 P3 P4
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C B A))
Line_on (Li B A) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P5 : "Def (Ang (An C B D))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C B A))
Line_on (Li B A) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An C B D))
[PROOF STEP]
have P6 : "Def (Ang (An D B C))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An C B D))

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

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B
[PROOF STEP]
have P8 : "Bet_Point (Se D A) B"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
from assms P5 P6 P7 P8
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B
Def (Ang (An C B D))
Def (Ang (An D B C))
Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An D B C)) add Emp)
Bet_Point (Se D A) B
[PROOF STEP]
have P9 : "Cong (Geos (Ang (An D B E)) add Emp) (Geos (Ang (An C B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
Bet_Point (Se A D) B
Bet_Point (Se C E) B
Def (Ang (An C B D))
Def (Ang (An D B C))
Cong (Geos (Ang (An C B D)) add Emp) (Geos (Ang (An D B C)) add Emp)
Bet_Point (Se D A) B

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An C B A)) add Emp)
[PROOF STEP]
have P10 : "Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An C B A)) add Emp)

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

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)
[PROOF STEP]
from P9 P10
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An D B E)) add Emp) (Geos (Ang (An C B A)) add Emp)
Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)
[PROOF STEP]
show "Cong (Geos (Ang (An A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An D B E)) add Emp) (Geos (Ang (An C B A)) add Emp)
Eq (Geos (Ang (An C B A)) add Emp) (Geos (Ang (An A B C)) add Emp)

goal (1 subgoal):
 1. Cong (Geos (Ang (An A B C)) 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 A B C)) add Emp) (Geos (Ang (An D B E)) add Emp)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_inside_Planeside :
  assumes "Ang_inside (An A B C) D"
  shows "Plane_diffside (Li B D) A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
[PROOF STEP]
have P1 : "Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P2 : "\<not> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P3 :  "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. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
[PROOF STEP]
have P4 : "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P2 P4
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) C
Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P5 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) C
Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B A) C

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P6 : "Line_on (Li B C) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) B

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P7 : "Line_on (Li B C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C

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

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

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

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) B \<and> Line_on (Li B C) E
[PROOF STEP]
have P9 : "Line_on (Li C E) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) B \<and> Line_on (Li B C) E

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P10 : "Line_on (Li C E) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C E) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C E) C

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P5 P6 P7 P9 P10
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B C) B
Line_on (Li B C) C
Line_on (Li C E) B
Line_on (Li C E) C
[PROOF STEP]
have P11 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B C) B
Line_on (Li B C) C
Line_on (Li C E) B
Line_on (Li C E) C

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P12 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P11 P12
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C E)) add Emp)
\<not> Line_on (Li B C) A
[PROOF STEP]
have P13 : "\<not> Line_on (Li C E) A"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C E)) add Emp)
\<not> Line_on (Li B C) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P14 : "Line_on (Li B D) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) B

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P15 : "\<not> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
[PROOF STEP]
have P16 : "Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P15 P16
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) D
Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) D
Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Line_on (Li B A) D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P6
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
[PROOF STEP]
have P18 : "Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) B

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P12 P18
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A
Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
have P19 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A
Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp) \<Longrightarrow> Line_on (Li B C) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P17 P19
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)
[PROOF STEP]
have P20 : "Line_on (Li B D) A \<Longrightarrow> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P15 P20
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) D
Line_on (Li B D) A \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P21 : "\<not> Line_on (Li B D) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) D
Line_on (Li B D) A \<Longrightarrow> Line_on (Li B A) D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P22 : "\<not> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P23 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P17 P23
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P24 : "Line_on (Li B D) C \<Longrightarrow> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P22 P24
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) D
Line_on (Li B D) C \<Longrightarrow> Line_on (Li B C) D
[PROOF STEP]
have P25 : "\<not> Line_on (Li B D) C"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) D
Line_on (Li B D) C \<Longrightarrow> Line_on (Li B C) D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) B \<and> Line_on (Li B C) E
[PROOF STEP]
have P26 : "Bet_Point (Se C E) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) B \<and> Line_on (Li B C) E

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

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

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) B \<and> Line_on (Li B C) E
[PROOF STEP]
have P28 : "Line_on (Li B C) E"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) B \<and> Line_on (Li B C) E

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P6 P14 P27 P28
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
Line_on (Li B D) B
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B C) E
[PROOF STEP]
have P29 : "Line_on (Li B D) E \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) B
Line_on (Li B D) B
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B C) E

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P7 P29
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) C
Line_on (Li B D) E \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B D)) add Emp)
[PROOF STEP]
have P30 : "Line_on (Li B D) E \<Longrightarrow> Line_on (Li B D) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) C
Line_on (Li B D) E \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B D)) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P25 P30
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B D) C
Line_on (Li B D) E \<Longrightarrow> Line_on (Li B D) C
[PROOF STEP]
have P31 : "\<not> Line_on (Li B D) E"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B D) C
Line_on (Li B D) E \<Longrightarrow> Line_on (Li B D) C

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P13 P14 P21 P25 P26 P31
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C E) A
Line_on (Li B D) B
\<not> Line_on (Li B D) A
\<not> Line_on (Li B D) C
Bet_Point (Se C E) B
\<not> Line_on (Li B D) E
[PROOF STEP]
have P32 : "Line_on_Seg (Li B D) (Se C A) \<and> \<not> Line_on_Seg (Li B D) (Se E A)
        \<or> Line_on_Seg (Li B D) (Se E A) \<and> \<not> Line_on_Seg (Li B D) (Se C A)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C E) A
Line_on (Li B D) B
\<not> Line_on (Li B D) A
\<not> Line_on (Li B D) C
Bet_Point (Se C E) B
\<not> Line_on (Li B D) E

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se C A) \<and> \<not> Line_on_Seg (Li B D) (Se E A) \<or> Line_on_Seg (Li B D) (Se E A) \<and> \<not> Line_on_Seg (Li B D) (Se C A)
[PROOF STEP]
by (simp add:Pachets_axiom)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se C A) \<and> \<not> Line_on_Seg (Li B D) (Se E A) \<or> Line_on_Seg (Li B D) (Se E A) \<and> \<not> Line_on_Seg (Li B D) (Se C A)

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<exists>p. Line_on (Li B D) p \<and> Bet_Point (Se E A) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<exists>p. Line_on (Li B D) p \<and> Bet_Point (Se E A) p
[PROOF STEP]
by (simp add:Line_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<exists>p. Line_on (Li B D) p \<and> Bet_Point (Se E A) p

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<exists>p. Line_on (Li B D) p \<and> Bet_Point (Se E A) p
[PROOF STEP]
obtain F :: Point where P33 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<exists>p. Line_on (Li B D) p \<and> Bet_Point (Se E A) p

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F
[PROOF STEP]
have P34 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se A E) F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se A E) F
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se A E) F

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
[PROOF STEP]
have P35 : "Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Line_on (Li A E) B"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P36 : "Line_on (Li A E) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A E) E
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A E) E

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P6 P27 P28 P35 P36
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B C) E
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Line_on (Li A E) B
Line_on (Li A E) E
[PROOF STEP]
have "Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) B
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B C) E
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Line_on (Li A E) B
Line_on (Li A E) E

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P37 : "Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P38 : "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. Plane_diffside (Li B D) A C
[PROOF STEP]
from P37 P38
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B A) A
[PROOF STEP]
have P39 : "Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Line_on (Li B A) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P12 P39
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) A
[PROOF STEP]
have P40 : "\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P37 P40
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P41 : "\<not> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li A E)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P34 P38 P41
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se A E) F
Line_on (Li B A) A
\<not> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P42 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B A) E F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se A E) F
Line_on (Li B A) A
\<not> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B A) E F
[PROOF STEP]
by (simp add:Plane_Bet_sameside Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B A) E F

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P11
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C E)) add Emp)
[PROOF STEP]
have P43 : "Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C E)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P40 P43
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P44 : "\<not> Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)
Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P3 P26 P44
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
Bet_Point (Se C E) B
\<not> Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P45 : "Plane_diffside (Li B A) E C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B
Bet_Point (Se C E) B
\<not> Eq (Geos (Lin (Li C E)) add Emp) (Geos (Lin (Li B A)) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P34
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se A E) F
[PROOF STEP]
have P46 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li A E) F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se A E) F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P47 : "Line_on (Li C E) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C E) E
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C E) E

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P48 : "Line_on (Li A E) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A E) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A E) A

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P42 P45
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B A) E F
Plane_diffside (Li B A) E C
[PROOF STEP]
have P49 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) F C"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B A) E F
Plane_diffside (Li B A) E C

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P50 : "Plane_sameside (Li B A) C D"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A) C D
[PROOF STEP]
have "Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> Plane_sameside (Li B A) C F"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A) C D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> Plane_sameside (Li B A) C F
[PROOF STEP]
have "Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) C F"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> Plane_sameside (Li B A) C F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) C F
[PROOF STEP]
have P51 : "Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) F C"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) C F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P49 P51
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) F C
Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) F C
[PROOF STEP]
have P52 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) F C
Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) F C

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P49 P50
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) F C
Plane_sameside (Li B A) C D
[PROOF STEP]
have P53 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) D F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) F C
Plane_sameside (Li B A) C D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P46
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li A E) F
[PROOF STEP]
have P54 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow>
    Line_on (Li A E) B"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li A E) F

goal (1 subgoal):
 1. \<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li A E) B
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li A E) B

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P26
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) B
[PROOF STEP]
have P55 : "Line_on (Li C E) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) B

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P27 P36 P47 P54 P55
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Line_on (Li A E) E
Line_on (Li C E) E
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li A E) B
Line_on (Li C E) B
[PROOF STEP]
have P56 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li C E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi E) add Emp) (Geos (Poi B) add Emp)
Line_on (Li A E) E
Line_on (Li C E) E
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li A E) B
Line_on (Li C E) B

goal (1 subgoal):
 1. \<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li C E)) add Emp)
[PROOF STEP]
by (simp add:Line_unique)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li C E)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P48 P56
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li A E) A
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li C E)) add Emp)
[PROOF STEP]
have P57 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp) \<Longrightarrow>
    Line_on (Li C E) A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li A E) A
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li C E)) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P13 P57
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C E) A
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li C E) A
[PROOF STEP]
have P58 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C E) A
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li C E) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P59 : "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. Plane_diffside (Li B D) A C
[PROOF STEP]
from P14 P17 P33 P52 P58 P59
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp)
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B D) D
[PROOF STEP]
have P60 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se B F) D \<or> Bet_Point (Se F D) B \<or> Bet_Point (Se D B) F"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp)
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B D) D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P61 : "Line_on (Li B F) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B F) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B F) B

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P62 : "Line_on (Li B F) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B F) F
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B F) F

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P33
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F
[PROOF STEP]
have P63 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P14 P58 P61 P62 P63
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) B
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B F) B
Line_on (Li B F) F
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F
[PROOF STEP]
have "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) B
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B F) B
Line_on (Li B F) F
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B D)) add Emp)
[PROOF STEP]
have P64 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B D)) add Emp)

goal (1 subgoal):
 1. \<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
by (blast intro:Eq_trans)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P38
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) A
[PROOF STEP]
have P65 : "Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp) \<Longrightarrow> Line_on (Li B D) A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P21 P65
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B D) A
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp) \<Longrightarrow> Line_on (Li B D) A
[PROOF STEP]
have P66 : "\<not> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B D) A
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp) \<Longrightarrow> Line_on (Li B D) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P64 P66
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)
\<not> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P67 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)
\<not> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P3 P67
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se B F) D \<Longrightarrow> Plane_sameside (Li B A) D F"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Eq (Geos (Lin (Li B F)) add Emp) (Geos (Lin (Li B A)) add Emp)

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se B F) D\<rbrakk> \<Longrightarrow> Plane_sameside (Li B A) D F
[PROOF STEP]
have P68 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se B F) D \<Longrightarrow> \<not> Plane_diffside (Li B A) D F"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se B F) D\<rbrakk> \<Longrightarrow> Plane_sameside (Li B A) D F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P53 P68
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) D F
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se B F) D\<rbrakk> \<Longrightarrow> \<not> Plane_diffside (Li B A) D F
[PROOF STEP]
have P69 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Bet_Point (Se B F) D"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) D F
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se B F) D\<rbrakk> \<Longrightarrow> \<not> Plane_diffside (Li B A) D F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have P70 : "Bet_Point (Se D B) F \<Longrightarrow> Bet_Point (Se B D) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se D B) F \<Longrightarrow> Bet_Point (Se B D) F
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se D B) F \<Longrightarrow> Bet_Point (Se B D) F

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P3 P66 P70
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
\<not> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)
Bet_Point (Se D B) F \<Longrightarrow> Bet_Point (Se B D) F
[PROOF STEP]
have "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se D B) F \<Longrightarrow> Plane_sameside (Li B A) D F"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B
\<not> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)
Bet_Point (Se D B) F \<Longrightarrow> Bet_Point (Se B D) F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se D B) F\<rbrakk> \<Longrightarrow> Plane_sameside (Li B A) D F
[PROOF STEP]
have P71 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se D B) F \<Longrightarrow> \<not> Plane_diffside (Li B A) D F"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se D B) F\<rbrakk> \<Longrightarrow> Plane_sameside (Li B A) D F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P53 P71
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) D F
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se D B) F\<rbrakk> \<Longrightarrow> \<not> Plane_diffside (Li B A) D F
[PROOF STEP]
have P72 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Bet_Point (Se D B) F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B A) D F
\<lbrakk>Line_on_Seg (Li B D) (Se E A); Bet_Point (Se D B) F\<rbrakk> \<Longrightarrow> \<not> Plane_diffside (Li B A) D F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P60 P69 P72
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se B F) D \<or> Bet_Point (Se F D) B \<or> Bet_Point (Se D B) F
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Bet_Point (Se B F) D
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Bet_Point (Se D B) F
[PROOF STEP]
have P73 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se F D) B"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se B F) D \<or> Bet_Point (Se F D) B \<or> Bet_Point (Se D B) F
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Bet_Point (Se B F) D
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Bet_Point (Se D B) F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have "Line_on (Li F D) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li F D) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li F D) D

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li F D) D
[PROOF STEP]
have P74 : "Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li F D) D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P22 P74
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) D
Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) D
[PROOF STEP]
have P75 : "\<not> Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) D
Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P6 P73 P75
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se F D) B
\<not> Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P76 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) F D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) B
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se F D) B
\<not> Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li B C)) add Emp)

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) F D
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) F D

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P33
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F
[PROOF STEP]
have P77 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se E A) F"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se E A) F

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
have "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. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li E A) A
[PROOF STEP]
have P78 : "Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li C E)) add Emp) \<Longrightarrow> Line_on (Li C E) A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li E A) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P13 P78
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li C E) A
Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li C E)) add Emp) \<Longrightarrow> Line_on (Li C E) A
[PROOF STEP]
have P79 : "\<not> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li C E)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li C E) A
Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li C E)) add Emp) \<Longrightarrow> Line_on (Li C E) A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P47 P77 P79
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li C E) E
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se E A) F
\<not> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li C E)) add Emp)
[PROOF STEP]
have P80 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li C E) F A"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li C E) E
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Bet_Point (Se E A) F
\<not> Eq (Geos (Lin (Li E A)) add Emp) (Geos (Lin (Li C E)) add Emp)

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li C E) F A
[PROOF STEP]
by (simp add:Plane_Bet_sameside)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li C E) F A

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P11 P80
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C E)) add Emp)
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li C E) F A
[PROOF STEP]
have P81 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B C) F A"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li C E)) add Emp)
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li C E) F A

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B C) F A
[PROOF STEP]
by (blast intro:Eq_rev Plane_Line_trans)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B C) F A

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P76 P81
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) F D
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B C) F A
[PROOF STEP]
have "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) A D"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) F D
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_sameside (Li B C) F A

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) A D
[PROOF STEP]
have P82 : "Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Plane_sameside (Li B C) A D"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> Plane_diffside (Li B C) A D

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Plane_sameside (Li B C) A D
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Plane_sameside (Li B C) A D

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P1 P82
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Plane_sameside (Li B C) A D
[PROOF STEP]
have P83 : "\<not> Line_on_Seg (Li B D) (Se E A)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
Line_on_Seg (Li B D) (Se E A) \<Longrightarrow> \<not> Plane_sameside (Li B C) A D

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P32 P83
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li B D) (Se C A) \<and> \<not> Line_on_Seg (Li B D) (Se E A) \<or> Line_on_Seg (Li B D) (Se E A) \<and> \<not> Line_on_Seg (Li B D) (Se C A)
\<not> Line_on_Seg (Li B D) (Se E A)
[PROOF STEP]
have "Line_on_Seg (Li B D) (Se C A)"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li B D) (Se C A) \<and> \<not> Line_on_Seg (Li B D) (Se E A) \<or> Line_on_Seg (Li B D) (Se E A) \<and> \<not> Line_on_Seg (Li B D) (Se C A)
\<not> Line_on_Seg (Li B D) (Se E A)

goal (1 subgoal):
 1. Line_on_Seg (Li B D) (Se C A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li B D) (Se C A)

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

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
from P21 P25 P84
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B D) A
\<not> Line_on (Li B D) C
\<exists>p. Line_on (Li B D) p \<and> Bet_Point (Se C A) p
[PROOF STEP]
have "\<exists>p. Bet_Point (Se C A) p \<and> Line_on (Li B D) p \<and> \<not> Line_on (Li B D) C \<and> \<not> Line_on (Li B D) A"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B D) A
\<not> Line_on (Li B D) C
\<exists>p. Line_on (Li B D) p \<and> Bet_Point (Se C A) p

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

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

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

goal (1 subgoal):
 1. Plane_diffside (Li B D) A C
[PROOF STEP]
thus "Plane_diffside (Li B D) A C"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B D) C A

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_inside_Bet_Point :
  assumes
    "Bet_Point (Se p1 p3) p2"
    "\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)"
    "\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)"
    "\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)"
  shows "Ang_inside (An p1 p4 p3) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
have P1 : "Line_on (Li p1 p3) p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p1 p3) p1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p3) p1

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
have P2 : "Line_on (Li p1 p3) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p1 p3) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p3) p3

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
have P3 : "Line_on (Li p4 p1) p4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p4 p1) p4
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p4 p1) p4

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
have P4 : "Line_on (Li p4 p1) p1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p4 p1) p1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p4 p1) p1

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
have P5 : "Line_on (Li p4 p3) p4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p4 p3) p4
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p4 p3) p4

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
have P6 : "Line_on (Li p4 p3) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p4 p3) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p4 p3) p3

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P7 : "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p3) p3
[PROOF STEP]
have P8 : "Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp) \<Longrightarrow> Line_on (Li p4 p1) p3"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p3) p3

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms P3 P5 P6 P8
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p1) p4
Line_on (Li p4 p3) p4
Line_on (Li p4 p3) p3
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp) \<Longrightarrow> Line_on (Li p4 p1) p3
[PROOF STEP]
have P9 : "Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p1) p4
Line_on (Li p4 p3) p4
Line_on (Li p4 p3) p3
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp) \<Longrightarrow> Line_on (Li p4 p1) p3

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms P9
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
[PROOF STEP]
have P10 : "\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p3) p1
[PROOF STEP]
have P11 : "Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp) \<Longrightarrow> Line_on (Li p4 p3) p1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p3) p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms P3 P4 P5 P11
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p1) p4
Line_on (Li p4 p1) p1
Line_on (Li p4 p3) p4
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp) \<Longrightarrow> Line_on (Li p4 p3) p1
[PROOF STEP]
have P12 : "Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p1) p4
Line_on (Li p4 p1) p1
Line_on (Li p4 p3) p4
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp) \<Longrightarrow> Line_on (Li p4 p3) p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms P12
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
[PROOF STEP]
have P13 : "\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms P4 P10
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p1) p1
\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp)
[PROOF STEP]
have "Plane_sameside (Li p4 p1) p2 p3"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p1) p1
\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p1)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li p4 p1) p2 p3
[PROOF STEP]
by (simp add:Plane_Bet_sameside)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p4 p1) p2 p3

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p4 p1) p2 p3
[PROOF STEP]
have P14 : "Plane_sameside (Li p4 p1) p3 p2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p4 p1) p2 p3

goal (1 subgoal):
 1. Plane_sameside (Li p4 p1) p3 p2
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p4 p1) p3 p2

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P15 : "Bet_Point (Se p3 p1) p2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p3 p1) p2
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p3 p1) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P16 : "Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p3 p1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from P13 P16
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p3 p1)) add Emp)
[PROOF STEP]
have P17 : "\<not> Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p3 p1)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms P6 P15 P17
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p3) p3
Bet_Point (Se p3 p1) p2
\<not> Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
[PROOF STEP]
have "Plane_sameside (Li p4 p3) p2 p1"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
Line_on (Li p4 p3) p3
Bet_Point (Se p3 p1) p2
\<not> Eq (Geos (Lin (Li p3 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li p4 p3) p2 p1
[PROOF STEP]
by (simp add:Plane_Bet_sameside)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p4 p3) p2 p1

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p4 p3) p2 p1
[PROOF STEP]
have P18 : "Plane_sameside (Li p4 p3) p1 p2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p4 p3) p2 p1

goal (1 subgoal):
 1. Plane_sameside (Li p4 p3) p1 p2
[PROOF STEP]
by (simp add:Plane_sameside_rev)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p4 p3) p1 p2

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P19 : "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from P7
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P20 : "\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from assms P19 P20
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
have P21 : "Def (Ang (An p1 p4 p3))"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p1 p3) p2
\<not> Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p4 p3)) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p1 p4 p3))
[PROOF STEP]
by (simp add:Ang_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p1 p4 p3))

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
from P14 P18 P21
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p4 p1) p3 p2
Plane_sameside (Li p4 p3) p1 p2
Def (Ang (An p1 p4 p3))
[PROOF STEP]
show "Ang_inside (An p1 p4 p3) p2"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p4 p1) p3 p2
Plane_sameside (Li p4 p3) p1 p2
Def (Ang (An p1 p4 p3))

goal (1 subgoal):
 1. Ang_inside (An p1 p4 p3) p2
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p1 p4 p3) p2

goal:
No subgoals!
[PROOF STEP]
qed