[STATEMENT]
lemma (in Congruence_Rule) Ang_inside_HalfLine :
  assumes
    "Ang_inside (An A B C) D"
    "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)"
    "Line_on (Li B D) E"
    "\<not> Bet_Point (Se E D) B"
  shows
    "Ang_inside (An A B C) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
[PROOF STEP]
have P1 : "Def (Ang (An A B C)) \<and> 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
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B

goal (1 subgoal):
 1. Def (Ang (An A B C)) \<and> 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:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
have P5 : "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. Ang_inside (An A B C) E
[PROOF STEP]
have P6 : "Line_on (Li E D) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li E D) E
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li E D) E

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
have P7 : "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. Ang_inside (An A B C) E
[PROOF STEP]
from assms P5 P6 P7
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
Line_on (Li B D) D
Line_on (Li E D) E
Line_on (Li E D) D
[PROOF STEP]
have P8 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow>
    Eq (Geos (Lin (Li E D)) add Emp) (Geos (Lin (Li B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
Line_on (Li B D) D
Line_on (Li E D) E
Line_on (Li E D) D

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
have P11 : "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. Ang_inside (An A B C) E
[PROOF STEP]
have P12 : "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. Ang_inside (An A B C) E
[PROOF STEP]
from P2 P4 P10 P11 P12
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) C E \<Longrightarrow> Bet_Point (Se D E) F \<and> Line_on (Li B A) F
Plane_diffside (Li B A) C E \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
\<lbrakk>Plane_diffside (Li B A) C E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B D) F
Line_on (Li B A) B
Line_on (Li B D) B
[PROOF STEP]
have P13 : "Plane_diffside (Li B A) C E \<Longrightarrow>
    \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) C E \<Longrightarrow> Bet_Point (Se D E) F \<and> Line_on (Li B A) F
Plane_diffside (Li B A) C E \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
\<lbrakk>Plane_diffside (Li B A) C E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B D) F
Line_on (Li B A) B
Line_on (Li B D) B

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C)) \<and> 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:
Def (Ang (An A B C)) \<and> 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. Ang_inside (An A B C) E
[PROOF STEP]
from P14 P15
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Plane_diffside (Li B A) C E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
\<not> Line_on (Li B A) D
[PROOF STEP]
have P16 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) C E"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Plane_diffside (Li B A) C E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
\<not> Line_on (Li B A) D

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from assms P18
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
\<lbrakk>Plane_diffside (Li B C) A E; Eq (Geos (Poi G) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se E D) B
[PROOF STEP]
have P19 : "Plane_diffside (Li B C) A E \<Longrightarrow> \<not> Eq (Geos (Poi G) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
\<lbrakk>Plane_diffside (Li B C) A E; Eq (Geos (Poi G) add Emp) (Geos (Poi B) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se E D) B

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
have P22 : "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. Ang_inside (An A B C) E
[PROOF STEP]
from P12 P17 P19 P21 P22
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) B
Plane_diffside (Li B C) A E \<Longrightarrow> Bet_Point (Se D E) G \<and> Line_on (Li B C) G
Plane_diffside (Li B C) A E \<Longrightarrow> \<not> Eq (Geos (Poi G) add Emp) (Geos (Poi B) add Emp)
\<lbrakk>Plane_diffside (Li B C) A E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B D) G
Line_on (Li B C) B
[PROOF STEP]
have P23 : "Plane_diffside (Li B C) A E \<Longrightarrow>
    \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)
    \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) B
Plane_diffside (Li B C) A E \<Longrightarrow> Bet_Point (Se D E) G \<and> Line_on (Li B C) G
Plane_diffside (Li B C) A E \<Longrightarrow> \<not> Eq (Geos (Poi G) add Emp) (Geos (Poi B) add Emp)
\<lbrakk>Plane_diffside (Li B C) A E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B D) G
Line_on (Li B C) B

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P25 : "\<not> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C)) \<and> 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. Ang_inside (An A B C) E
[PROOF STEP]
from P24 P25
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Plane_diffside (Li B C) A E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B C) D
\<not> Line_on (Li B C) D
[PROOF STEP]
have P26 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B C) A E"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Plane_diffside (Li B C) A E; \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B C) D
\<not> Line_on (Li B C) D

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P27 : "\<not> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C)) \<and> 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. Ang_inside (An A B C) E
[PROOF STEP]
from P8 P12
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li E D)) add Emp) (Geos (Lin (Li B D)) add Emp)
Line_on (Li B D) B
[PROOF STEP]
have P28 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li E D) B"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li E D)) add Emp) (Geos (Lin (Li B D)) add Emp)
Line_on (Li B D) B

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P15 P30
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) D
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Line_on (Li B A) E\<rbrakk> \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P31 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow>
    \<not> Line_on (Li B A) E"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) D
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Line_on (Li B A) E\<rbrakk> \<Longrightarrow> Line_on (Li B A) D

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P32 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
have P33 : "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. Ang_inside (An A B C) E
[PROOF STEP]
from P12 P22 P32 P33
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) B
Line_on (Li B C) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B C) C
[PROOF STEP]
have P34 : "Line_on (Li B D) C \<Longrightarrow>
    Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) B
Line_on (Li B C) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Line_on (Li B C) C

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P5 P34
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) D
Line_on (Li B D) C \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P35 : "Line_on (Li B D) C \<Longrightarrow> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) D
Line_on (Li B D) C \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li B 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_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) C \<Longrightarrow> Line_on (Li B C) D

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P25 P35
[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 P36 : "\<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. Ang_inside (An A B C) E
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
[PROOF STEP]
have P37 : "Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B D) C"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P36 P37
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B D) C
Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B D) C
[PROOF STEP]
have P38 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi E) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B D) C
Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Line_on (Li B D) C

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P16 P27 P31 P38
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) C E
\<not> Line_on (Li B A) C
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B A) E
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi E) add Emp)
[PROOF STEP]
have P39 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow>
    Plane_sameside (Li B A) C E"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B A) C E
\<not> Line_on (Li B A) C
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B A) E
\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi E) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
[PROOF STEP]
have P40 : "\<not> Line_on (Li B C) A"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C)) \<and> 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. Ang_inside (An A B C) E
[PROOF STEP]
from assms P6 P22 P28
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
Line_on (Li E D) E
Line_on (Li B C) B
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li E D) B
[PROOF STEP]
have P41 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li B C) E \<Longrightarrow>
    Eq (Geos (Lin (Li E D)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi E) add Emp)
Line_on (Li B D) E
\<not> Bet_Point (Se E D) B
Line_on (Li E D) E
Line_on (Li B C) B
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Line_on (Li E D) B

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P7 P41
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li E D) D
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Line_on (Li B C) E\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li E D)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P42 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow>
    Line_on (Li B C) E \<Longrightarrow> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li E D) D
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Line_on (Li B C) E\<rbrakk> \<Longrightarrow> Eq (Geos (Lin (Li E D)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P25 P42
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) D
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Line_on (Li B C) E\<rbrakk> \<Longrightarrow> Line_on (Li B C) D
[PROOF STEP]
have P43 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B C) E"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) D
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Line_on (Li B C) E\<rbrakk> \<Longrightarrow> Line_on (Li B C) D

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P39
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Plane_sameside (Li B A) C E
[PROOF STEP]
have P44 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B A) E"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Plane_sameside (Li B A) C E

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P44 P45
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B A) E
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B A) E
[PROOF STEP]
have P46 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow>
    \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B A) E
\<lbrakk>\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp); Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B A) E

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P26 P40 P43 P46
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B C) A E
\<not> Line_on (Li B C) A
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B C) E
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)
[PROOF STEP]
have P47 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow>
    Plane_sameside (Li B C) A E"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B C) A E
\<not> Line_on (Li B C) A
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Line_on (Li B C) E
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> \<not> Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P1 P39 P47
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Plane_sameside (Li B A) C E
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Plane_sameside (Li B C) A E
[PROOF STEP]
have P48 : "\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Ang_inside (An A B C) E"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C)) \<and> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Plane_sameside (Li B A) C E
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Plane_sameside (Li B C) A E

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A B C) E
[PROOF STEP]
from P48 P49
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Ang_inside (An A B C) E
Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Ang_inside (An A B C) E
[PROOF STEP]
show "Ang_inside (An A B C) E"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Ang_inside (An A B C) E
Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) \<Longrightarrow> Ang_inside (An A B C) E

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Ang_outside_Planeside :
  assumes
    "Def (Ang (An A B C))"
    "\<not> Ang_inside (An A B C) D"
  shows "\<not> (Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D)"
  and "\<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
      \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
      \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D) &&& \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> (Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D)
 2. \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
\<not> 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 \<Longrightarrow> Ang_inside (An A B C) D"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
\<not> 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 \<Longrightarrow> Ang_inside (An A B C) 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 \<Longrightarrow> Ang_inside (An A B C) D

goal (2 subgoals):
 1. \<not> (Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D)
 2. \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
\<not> Ang_inside (An A B C) D
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<Longrightarrow> Ang_inside (An A B C) D
[PROOF STEP]
show "\<not> (Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))
\<not> Ang_inside (An A B C) D
Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<Longrightarrow> Ang_inside (An A B C) D

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

goal (1 subgoal):
 1. \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
[PROOF STEP]
thus "\<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
      \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
      \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D"
[PROOF STATE]
proof (prove)
using this:
\<not> (Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D)

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

goal:
No subgoals!
[PROOF STEP]
qed