[STATEMENT]
lemma (in Congruence_Rule) Seg_Plane_sameside :
  assumes
    "Line_on l1 A"
    "Line_on l1 B"
    "Line_on l1 C"
    "\<not> Line_on l1 D"
    "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
    "\<not> Bet_Point (Se B C) A"
  shows "Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have "Line_on (Li D A) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D A) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D A) D

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P9 : "Line_on (Li D A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li D A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li D A) A

goal (1 subgoal):
 1. Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from assms P2 P3 P8 P9
[PROOF STATE]
proof (chain)
picking this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Line_on l1 D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Eq (Geos (Lin (Li D A)) add Emp) (Geos (Lin l1) add Emp)
Plane_diffside (Li D A) B C \<Longrightarrow> Bet_Point (Se B C) E \<and> Line_on (Li D A) E
\<lbrakk>Plane_diffside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 E
Line_on (Li D A) A
[PROOF STEP]
have P10 : "Plane_diffside (Li D A) B C \<Longrightarrow> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow>
    Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Line_on l1 D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Eq (Geos (Lin (Li D A)) add Emp) (Geos (Lin l1) add Emp)
Plane_diffside (Li D A) B C \<Longrightarrow> Bet_Point (Se B C) E \<and> Line_on (Li D A) E
\<lbrakk>Plane_diffside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 E
Line_on (Li D A) A

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

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

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

goal (1 subgoal):
 1. Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from P10 P11
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Plane_diffside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Plane_diffside (Li D A) B C \<Longrightarrow> Bet_Point (Se B C) E
[PROOF STEP]
have P12 : "Plane_diffside (Li D A) B C \<Longrightarrow> \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow>
    Bet_Point (Se B C) A"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Plane_diffside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)\<rbrakk> \<Longrightarrow> Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp)
Plane_diffside (Li D A) B C \<Longrightarrow> Bet_Point (Se B C) E

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P3 : "Line_on (Li A B) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) A

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P4 : "Line_on (Li A B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A B) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A B) B

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from assms P7
[PROOF STATE]
proof (chain)
picking this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Line_on (Li A B) D
[PROOF STEP]
have "Def (Tri (Tr A B D))"
[PROOF STATE]
proof (prove)
using this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Line_on (Li A B) D

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B D))
[PROOF STEP]
have "Def (Tri (Tr D B A))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B D))

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr D B A))
[PROOF STEP]
have P12 : "Def (Tri (Tr A D B))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr D B A))

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P13 : "Line_on (Li A C) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A C) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A C) A

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from assms P13 P14
[PROOF STATE]
proof (chain)
picking this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
Line_on (Li A C) A
Line_on (Li A C) C
[PROOF STEP]
have P15 : "Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li A C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
Line_on (Li A C) A
Line_on (Li A C) C

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from assms P16
[PROOF STATE]
proof (chain)
picking this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Line_on (Li A C) D
[PROOF STEP]
have "Def (Tri (Tr A C D))"
[PROOF STATE]
proof (prove)
using this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Line_on (Li A C) D

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A C D))
[PROOF STEP]
have "Def (Tri (Tr D C A))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A C D))

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr D C A))
[PROOF STEP]
have P17 : "Def (Tri (Tr A D C))"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr D C A))

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Line_on l1 D
[PROOF STEP]
have P22 : "Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
\<not> Line_on l1 D

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from P19 P21
[PROOF STATE]
proof (chain)
picking this:
Cong (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An B D A)) add Emp)
Cong (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An C D A)) add Emp)
[PROOF STEP]
have P23 : "Plane_sameside (Li D A) B C \<Longrightarrow> Eq (Geos (Lin (Li B D)) add Emp) (Geos (Lin (Li C D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Cong (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An B D A)) add Emp)
Cong (Geos (Ang (An A D B)) add Emp) (Geos (Ang (An C D A)) add Emp)

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P26 : "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. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P27 : "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. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P28 : "Line_on (Li C D) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C D) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C D) C

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P30 : "Line_on (Li C D) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C D) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C D) D

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

goal (1 subgoal):
 1. \<lbrakk>Plane_sameside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) 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_sameside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)\<rbrakk> \<Longrightarrow> Line_on (Li B C) D

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from assms P26 P27
[PROOF STATE]
proof (chain)
picking this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
Line_on (Li B C) B
Line_on (Li B C) C
[PROOF STEP]
have P32 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin l1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on l1 A
Line_on l1 B
Line_on l1 C
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)
Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
\<not> Bet_Point (Se B C) A
Line_on (Li B C) B
Line_on (Li B C) C

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

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

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from P1 P33
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on l1 D
\<lbrakk>Plane_sameside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 D
[PROOF STEP]
have P34 : "Plane_sameside (Li D A) B C \<Longrightarrow> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on l1 D
\<lbrakk>Plane_sameside (Li D A) B C; \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)\<rbrakk> \<Longrightarrow> Line_on l1 D

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

goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from P22 P34
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Plane_sameside (Li D A) B C \<Longrightarrow> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
show "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li D A) B C \<or> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
Plane_sameside (Li D A) B C \<Longrightarrow> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Seg_not_Eq_Point :
  assumes
    "\<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)"
  shows "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P1 : "Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow>
    Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
[PROOF STEP]
by (simp add:Seg_Point_Eq)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
[PROOF STEP]
show "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)
Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp) \<Longrightarrow> Eq (Geos (Seg (Se A B)) add Emp) (Geos (Seg (Se A C)) add Emp)

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

goal:
No subgoals!
[PROOF STEP]
qed