[STATEMENT]
lemma (in Congruence_Rule) Seg_Bet_move_diffside :
  assumes
    "Bet_Point (Se p11 p13) p12"
    "Line_on l1 p21" "Line_on l1 p4"
    "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)"
  shows "\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q
    \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp)
    \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)
[PROOF STEP]
have P1 : "\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p12) add Emp) (Geos (Poi p11) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms P1
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p12) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by (simp add:Seg_move_diffside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain p22 :: Point where P2 : "Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
    \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>p22. Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p13) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms P2 P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p13) add Emp)
[PROOF STEP]
have "\<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
\<not> Eq (Geos (Poi p11) add Emp) (Geos (Poi p13) add Emp)

goal (1 subgoal):
 1. \<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
by (simp add:Seg_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)
[PROOF STEP]
obtain p23 :: Point where P4 : "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
    \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> Line_on l1 p \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p) add Emp)

goal (1 subgoal):
 1. (\<And>p23. Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from P4
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
have "\<not> Bet_Point (Se p23 p22) p21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. \<not> Bet_Point (Se p23 p22) p21
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se p23 p22) p21

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Bet_Point (Se p23 p22) p21
[PROOF STEP]
have P5 : "\<not> Bet_Point (Se p22 p23) p21"
[PROOF STATE]
proof (prove)
using this:
\<not> Bet_Point (Se p23 p22) p21

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

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from assms P2 P4 P5
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
\<not> Bet_Point (Se p22 p23) p21
[PROOF STEP]
have P6 : "Bet_Point (Se p21 p23) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Line_on l1 p21
Line_on l1 p4
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p4) add Emp)
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
\<not> Bet_Point (Se p22 p23) p21

goal (1 subgoal):
 1. Bet_Point (Se p21 p23) p22
[PROOF STEP]
by (blast intro:Seg_Bet_move_lemma1)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p21 p23) p22

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 p23) p22
[PROOF STEP]
have P7 : "Bet_Point (Se p23 p21) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 p23) p22

goal (1 subgoal):
 1. Bet_Point (Se p23 p21) p22
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from P2 P7
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Bet_Point (Se p23 p21) p22
[PROOF STEP]
have P8 : "Bet_Point (Se p23 p4) p21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. Bet_Point (Se p23 p4) p21
[PROOF STEP]
by (blast intro:Bet_swap_234_134)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p23 p4) p21

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
from P2 P4 P6 P8
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Bet_Point (Se p21 p23) p22
Bet_Point (Se p23 p4) p21
[PROOF STEP]
show "\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q
    \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp)
    \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp) \<and> Bet_Point (Se p22 p4) p21 \<and> Line_on l1 p22 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp) \<and> \<not> Bet_Point (Se p23 p22) p21 \<and> Line_on l1 p23 \<and> \<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
Bet_Point (Se p21 p23) p22
Bet_Point (Se p23 p4) p21

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on l1 p \<and> Line_on l1 q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> Bet_Point (Se p p4) p21 \<and> Bet_Point (Se q p4) p21

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Congruence_Rule) Seg_Bet_wrong_relation :
  assumes
    "Bet_Point (Se p11 p13) p12"
    "Bet_Point (Se p21 p22) p23"
    "Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)"
    "Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
  shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have P1 : "Line_on (Li p21 p22) p21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p21 p22) p21
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p21 p22) p21

goal (1 subgoal):
 1. False
[PROOF STEP]
have P2 : "Line_on (Li p21 p22) p22"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p21 p22) p22
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p21 p22) p22

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
have P3 : "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms P1 P2 P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
Line_on (Li p21 p22) p21
Line_on (Li p21 p22) p22
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
[PROOF STEP]
have "\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on (Li p21 p22) p \<and> Line_on (Li p21 p22) q
    \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp)
    \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp)
    \<and> \<not> Bet_Point (Se p p22) p21 \<and> \<not> Bet_Point (Se q p22) p21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
Line_on (Li p21 p22) p21
Line_on (Li p21 p22) p22
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)

goal (1 subgoal):
 1. \<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on (Li p21 p22) p \<and> Line_on (Li p21 p22) q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> \<not> Bet_Point (Se q p22) p21
[PROOF STEP]
by (simp add:Seg_Bet_move_sameside)
[PROOF STATE]
proof (state)
this:
\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on (Li p21 p22) p \<and> Line_on (Li p21 p22) q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> \<not> Bet_Point (Se q p22) p21

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on (Li p21 p22) p \<and> Line_on (Li p21 p22) q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> \<not> Bet_Point (Se q p22) p21
[PROOF STEP]
obtain pn2 pn3 :: Point where P4 : "Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3
    \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp)
    \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp)
    \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21"
[PROOF STATE]
proof (prove)
using this:
\<exists>p q. Bet_Point (Se p21 q) p \<and> Line_on (Li p21 p22) p \<and> Line_on (Li p21 p22) q \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 q)) add Emp) \<and> \<not> Bet_Point (Se p p22) p21 \<and> \<not> Bet_Point (Se q p22) p21

goal (1 subgoal):
 1. (\<And>pn3 pn2. Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
[PROOF STEP]
have P5 : "Bet_Point (Se p21 pn3) pn2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21

goal (1 subgoal):
 1. Bet_Point (Se p21 pn3) pn2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p21 pn3) pn2

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 pn3) pn2
[PROOF STEP]
have "\<not> Eq (Geos (Poi pn2) add Emp) (Geos (Poi p21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 pn3) pn2

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

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi pn2) add Emp) (Geos (Poi p21) add Emp)
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi pn2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi pn2) add Emp) (Geos (Poi p21) add Emp)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms P4
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
[PROOF STEP]
have P7 : "Eq (Geos (Seg (Se p21 pn2)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1 P2 P3 P4 P6 P7
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p21 p22) p21
Line_on (Li p21 p22) p22
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi pn2) add Emp)
Eq (Geos (Seg (Se p21 pn2)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
[PROOF STEP]
have P8 : "Eq (Geos (Poi pn2) add Emp) (Geos (Poi p22) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p21 p22) p21
Line_on (Li p21 p22) p22
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p22) add Emp)
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi pn2) add Emp)
Eq (Geos (Seg (Se p21 pn2)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi pn2) add Emp) (Geos (Poi p22) add Emp)
[PROOF STEP]
by (blast intro:Seg_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi pn2) add Emp) (Geos (Poi p22) add Emp)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P5 P8
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 pn3) pn2
Eq (Geos (Poi pn2) add Emp) (Geos (Poi p22) add Emp)
[PROOF STEP]
have "Bet_Point (Se p21 pn3) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 pn3) pn2
Eq (Geos (Poi pn2) add Emp) (Geos (Poi p22) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p21 pn3) p22
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p21 pn3) p22

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 pn3) p22
[PROOF STEP]
have P9 : "Bet_Point (Se pn3 p21) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 pn3) p22

goal (1 subgoal):
 1. Bet_Point (Se pn3 p21) p22
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn3 p21) p22

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
have P10 : "Line_on (Li p21 p22) p23"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)

goal (1 subgoal):
 1. Line_on (Li p21 p22) p23
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p21 p22) p23

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
have "\<not> Eq (Geos (Poi p23) add Emp) (Geos (Poi p21) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p23) add Emp) (Geos (Poi p21) add Emp)
[PROOF STEP]
have P11 : "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p23) add Emp) (Geos (Poi p21) add Emp)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 pn3) pn2
[PROOF STEP]
have P12 : "\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi pn3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 pn3) pn2

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms P4
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
[PROOF STEP]
have P13 : "Eq (Geos (Seg (Se p21 pn3)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
have P14 : "Bet_Point (Se p22 p21) p23"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p22 p21) p23
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p22 p21) p23

goal (1 subgoal):
 1. False
[PROOF STEP]
have P15 : "Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p23 pn3) p21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p23 pn3) p21
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p23 pn3) p21

goal (1 subgoal):
 1. False
[PROOF STEP]
from P14 P15
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p22 p21) p23
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p23 pn3) p21
[PROOF STEP]
have "Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p22 pn3) p21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p22 p21) p23
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p23 pn3) p21

goal (1 subgoal):
 1. Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p22 pn3) p21
[PROOF STEP]
by (blast intro:Bet_swap_234_134)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p22 pn3) p21

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p22 pn3) p21
[PROOF STEP]
have P16 : "Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se pn3 p22) p21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se p22 pn3) p21

goal (1 subgoal):
 1. Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se pn3 p22) p21
[PROOF STEP]
by (simp add:Bet_rev)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se pn3 p22) p21

goal (1 subgoal):
 1. False
[PROOF STEP]
from P4 P16
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se pn3 p22) p21
[PROOF STEP]
have P17 : "\<not> Bet_Point (Se pn3 p23) p21"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
Bet_Point (Se pn3 p23) p21 \<Longrightarrow> Bet_Point (Se pn3 p22) p21

goal (1 subgoal):
 1. \<not> Bet_Point (Se pn3 p23) p21
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Bet_Point (Se pn3 p23) p21

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1 P4 P10 P11 P12 P13 P17
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p21 p22) p21
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
Line_on (Li p21 p22) p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi pn3) add Emp)
Eq (Geos (Seg (Se p21 pn3)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se pn3 p23) p21
[PROOF STEP]
have P18 : "Eq (Geos (Poi pn3) add Emp) (Geos (Poi p23) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p21 p22) p21
Bet_Point (Se p21 pn3) pn2 \<and> Line_on (Li p21 p22) pn2 \<and> Line_on (Li p21 p22) pn3 \<and> Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 pn2)) add Emp) \<and> Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 pn3)) add Emp) \<and> \<not> Bet_Point (Se pn2 p22) p21 \<and> \<not> Bet_Point (Se pn3 p22) p21
Line_on (Li p21 p22) p23
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi p23) add Emp)
\<not> Eq (Geos (Poi p21) add Emp) (Geos (Poi pn3) add Emp)
Eq (Geos (Seg (Se p21 pn3)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
\<not> Bet_Point (Se pn3 p23) p21

goal (1 subgoal):
 1. Eq (Geos (Poi pn3) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
by (blast intro:Seg_move_unique)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi pn3) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P9 P18
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se pn3 p21) p22
Eq (Geos (Poi pn3) add Emp) (Geos (Poi p23) add Emp)
[PROOF STEP]
have P19 : "Bet_Point (Se p23 p21) p22"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se pn3 p21) p22
Eq (Geos (Poi pn3) add Emp) (Geos (Poi p23) add Emp)

goal (1 subgoal):
 1. Bet_Point (Se p23 p21) p22
[PROOF STEP]
by (simp add:Bet_Point_Eq)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)
[PROOF STEP]
have "Inv (Bet_Point (Se p22 p23) p21) \<and> Inv (Bet_Point (Se p23 p21) p22)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p11 p13) p12
Bet_Point (Se p21 p22) p23
Eq (Geos (Seg (Se p11 p12)) add Emp) (Geos (Seg (Se p21 p22)) add Emp)
Eq (Geos (Seg (Se p11 p13)) add Emp) (Geos (Seg (Se p21 p23)) add Emp)

goal (1 subgoal):
 1. Inv (Bet_Point (Se p22 p23) p21) \<and> Inv (Bet_Point (Se p23 p21) p22)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se p22 p23) p21) \<and> Inv (Bet_Point (Se p23 p21) p22)

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se p22 p23) p21) \<and> Inv (Bet_Point (Se p23 p21) p22)
[PROOF STEP]
have P20 : "\<not> Bet_Point (Se p23 p21) p22"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se p22 p23) p21) \<and> Inv (Bet_Point (Se p23 p21) p22)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P19 P20
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p23 p21) p22
\<not> Bet_Point (Se p23 p21) p22
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p23 p21) p22
\<not> Bet_Point (Se p23 p21) p22

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P4 : "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 A1 B C1) D
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
Def (Ang (An A B C))
Line_on (Li B A1) A
\<not> Bet_Point (Se A A1) B
Line_on (Li B C1) C
\<not> Bet_Point (Se C C1) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C1) add Emp)
[PROOF STEP]
have P5 : "Def (Tri (Tr A B C))"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D
Def (Ang (An A B C))
Line_on (Li B A1) A
\<not> Bet_Point (Se A A1) B
Line_on (Li B C1) C
\<not> Bet_Point (Se C C1) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C1) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P10 : "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 A1 B C1) D
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr A B C))
[PROOF STEP]
have P11 : "\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr A B C))

goal (1 subgoal):
 1. \<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
by (simp add:Tri_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 A1 B C1) D
[PROOF STEP]
from assms P8 P9 P10 P11
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
Def (Ang (An A B C))
Line_on (Li B A1) A
\<not> Bet_Point (Se A A1) B
Line_on (Li B C1) C
\<not> Bet_Point (Se C C1) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B C) B
Line_on (Li B C1) B
Line_on (Li B C) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
[PROOF STEP]
have P12 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B C1)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D
Def (Ang (An A B C))
Line_on (Li B A1) A
\<not> Bet_Point (Se A A1) B
Line_on (Li B C1) C
\<not> Bet_Point (Se C C1) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B C) B
Line_on (Li B C1) B
Line_on (Li B C) C
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P13 : "Plane_diffside (Li B A) C1 D \<Longrightarrow> Plane_diffside (Li B A) D C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_diffside (Li B A) C1 D \<Longrightarrow> Plane_diffside (Li B A) D C1
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B A) C1 D \<Longrightarrow> Plane_diffside (Li B A) D C1

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P13 P14
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) C1 D \<Longrightarrow> Plane_diffside (Li B A) D C1
Plane_sameside (Li B A) D C
[PROOF STEP]
have P15 : "Plane_diffside (Li B A) C1 D \<Longrightarrow> Plane_diffside (Li B A) C C1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) C1 D \<Longrightarrow> Plane_diffside (Li B A) D C1
Plane_sameside (Li B A) D C

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P19 : "Line_on (Li B C1) C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B C1) C1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C1) C1

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P20 : "Line_on (Li C C1) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C C1) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C C1) C

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P21 : "Line_on (Li C C1) C1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C C1) C1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C C1) C1

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P16 P24
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) C1 D \<Longrightarrow> Bet_Point (Se C C1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) C1
Eq (Geos (Lin (Li C C1)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) C1
[PROOF STEP]
have P25 : "Plane_diffside (Li B A) C1 D \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li C C1)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) C1 D \<Longrightarrow> Bet_Point (Se C C1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) C1
Eq (Geos (Lin (Li C C1)) add Emp) (Geos (Lin (Li B A)) add Emp) \<Longrightarrow> Line_on (Li B A) C1

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P2 P16 P18 P23 P25
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) B
Plane_diffside (Li B A) C1 D \<Longrightarrow> Bet_Point (Se C C1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) C1
Plane_diffside (Li B A) C1 D \<Longrightarrow> Line_on (Li C C1) B1
\<lbrakk>\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi C1) add Emp); Plane_diffside (Li B A) C1 D\<rbrakk> \<Longrightarrow> Line_on (Li C C1) B
Plane_diffside (Li B A) C1 D \<Longrightarrow> \<not> Eq (Geos (Lin (Li C C1)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P26 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi C1) add Emp) \<Longrightarrow>
    Plane_diffside (Li B A) C1 D \<Longrightarrow> Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) B
Plane_diffside (Li B A) C1 D \<Longrightarrow> Bet_Point (Se C C1) B1 \<and> Line_on (Li B A) B1 \<and> \<not> Line_on (Li B A) C \<and> \<not> Line_on (Li B A) C1
Plane_diffside (Li B A) C1 D \<Longrightarrow> Line_on (Li C C1) B1
\<lbrakk>\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi C1) add Emp); Plane_diffside (Li B A) C1 D\<rbrakk> \<Longrightarrow> Line_on (Li C C1) B
Plane_diffside (Li B A) C1 D \<Longrightarrow> \<not> Eq (Geos (Lin (Li C C1)) add Emp) (Geos (Lin (Li B A)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P17 P26
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B A) C1 D \<Longrightarrow> Bet_Point (Se C C1) B1
\<lbrakk>\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi C1) add Emp); Plane_diffside (Li B A) C1 D\<rbrakk> \<Longrightarrow> Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P27 : "\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi C1) add Emp) \<Longrightarrow>
    Plane_diffside (Li B A) C1 D \<Longrightarrow> Bet_Point (Se C C1) B"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B A) C1 D \<Longrightarrow> Bet_Point (Se C C1) B1
\<lbrakk>\<not> Eq (Geos (Poi C) add Emp) (Geos (Poi C1) add Emp); Plane_diffside (Li B A) C1 D\<rbrakk> \<Longrightarrow> Eq (Geos (Poi B1) add Emp) (Geos (Poi B) add Emp)

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P10 P30
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) C
Line_on (Li B A) C1 \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P31 : "Line_on (Li B A) C1 \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) C
Line_on (Li B A) C1 \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp)

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P31 P32
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) C1 \<Longrightarrow> Line_on (Li B A) C
\<not> Line_on (Li B A) C
[PROOF STEP]
have P33 : "\<not> Line_on (Li B A) C1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) C1 \<Longrightarrow> Line_on (Li B A) C
\<not> Line_on (Li B A) C

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P12 P19
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B C1)) add Emp)
Line_on (Li B C1) C1
[PROOF STEP]
have "Line_on (Li B C) C1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B C1)) add Emp)
Line_on (Li B C1) C1

goal (1 subgoal):
 1. Line_on (Li B C) C1
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C) C1

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) C1
[PROOF STEP]
have P35 : "Eq (Geos (Poi C1) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Line_on (Li B C) D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) C1

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P7 P40
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B A1)) add Emp)
Plane_sameside (Li B A) C1 D
[PROOF STEP]
have P41 : "Plane_sameside (Li B A1) C1 D"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B A1)) add Emp)
Plane_sameside (Li B A) C1 D

goal (1 subgoal):
 1. Plane_sameside (Li B A1) C1 D
[PROOF STEP]
by (simp add:Plane_Line_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li B A1) C1 D

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P42 : "Plane_diffside (Li B C) A1 D \<Longrightarrow> Plane_diffside (Li B C) D A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_diffside (Li B C) A1 D \<Longrightarrow> Plane_diffside (Li B C) D A1
[PROOF STEP]
by (simp add:Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Plane_diffside (Li B C) D A1

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P42 P43
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Plane_diffside (Li B C) D A1
Plane_sameside (Li B C) D A
[PROOF STEP]
have P44 : "Plane_diffside (Li B C) A1 D \<Longrightarrow> Plane_diffside (Li B C) A A1"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Plane_diffside (Li B C) D A1
Plane_sameside (Li B C) D A

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P45
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2 \<and> Line_on (Li B C) B2 \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li B C) A1
[PROOF STEP]
have P46 : "Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2 \<and> Line_on (Li B C) B2 \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li B C) A1

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P48 : "Line_on (Li B A1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B A1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A1) A1

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P49 : "Line_on (Li A A1) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A A1) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A A1) A

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
have P50 : "Line_on (Li A A1) A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li A A1) A1
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li A A1) A1

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P45 P53
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2 \<and> Line_on (Li B C) B2 \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li B C) A1
Eq (Geos (Lin (Li A A1)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) A1
[PROOF STEP]
have P54 : "Plane_diffside (Li B C) A1 D \<Longrightarrow>
    \<not> Eq (Geos (Lin (Li A A1)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2 \<and> Line_on (Li B C) B2 \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li B C) A1
Eq (Geos (Lin (Li A A1)) add Emp) (Geos (Lin (Li B C)) add Emp) \<Longrightarrow> Line_on (Li B C) A1

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P8 P45 P47 P52 P54
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2 \<and> Line_on (Li B C) B2 \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li B C) A1
Plane_diffside (Li B C) A1 D \<Longrightarrow> Line_on (Li A A1) B2
\<lbrakk>\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp); Plane_diffside (Li B C) A1 D\<rbrakk> \<Longrightarrow> Line_on (Li A A1) B
Plane_diffside (Li B C) A1 D \<Longrightarrow> \<not> Eq (Geos (Lin (Li A A1)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P55 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow>
    Plane_diffside (Li B C) A1 D \<Longrightarrow> Eq (Geos (Poi B2) add Emp) (Geos (Poi B) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) B
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2 \<and> Line_on (Li B C) B2 \<and> \<not> Line_on (Li B C) A \<and> \<not> Line_on (Li B C) A1
Plane_diffside (Li B C) A1 D \<Longrightarrow> Line_on (Li A A1) B2
\<lbrakk>\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp); Plane_diffside (Li B C) A1 D\<rbrakk> \<Longrightarrow> Line_on (Li A A1) B
Plane_diffside (Li B C) A1 D \<Longrightarrow> \<not> Eq (Geos (Lin (Li A A1)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P46 P55
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2
\<lbrakk>\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp); Plane_diffside (Li B C) A1 D\<rbrakk> \<Longrightarrow> Eq (Geos (Poi B2) add Emp) (Geos (Poi B) add Emp)
[PROOF STEP]
have P56 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow>
    Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li B C) A1 D \<Longrightarrow> Bet_Point (Se A A1) B2
\<lbrakk>\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp); Plane_diffside (Li B C) A1 D\<rbrakk> \<Longrightarrow> Eq (Geos (Poi B2) add Emp) (Geos (Poi B) add Emp)

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from assms P3 P8 P48
[PROOF STATE]
proof (chain)
picking this:
Ang_inside (An A B C) D
Def (Ang (An A B C))
Line_on (Li B A1) A
\<not> Bet_Point (Se A A1) B
Line_on (Li B C1) C
\<not> Bet_Point (Se C C1) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B A1) B
Line_on (Li B C) B
Line_on (Li B A1) A1
[PROOF STEP]
have P58 : "Line_on (Li B C) A1 \<Longrightarrow>
    Eq (Geos (Lin (Li B A1)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Ang_inside (An A B C) D
Def (Ang (An A B C))
Line_on (Li B A1) A
\<not> Bet_Point (Se A A1) B
Line_on (Li B C1) C
\<not> Bet_Point (Se C C1) B
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi A1) add Emp)
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C1) add Emp)
Line_on (Li B A1) B
Line_on (Li B C) B
Line_on (Li B A1) A1

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P7 P58
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B A1)) add Emp)
Line_on (Li B C) A1 \<Longrightarrow> Eq (Geos (Lin (Li B A1)) add Emp) (Geos (Lin (Li B C)) add Emp)
[PROOF STEP]
have P59 : "Line_on (Li B C) A1 \<Longrightarrow>
    Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B A1)) add Emp)
Line_on (Li B C) A1 \<Longrightarrow> Eq (Geos (Lin (Li B A1)) add Emp) (Geos (Lin (Li B C)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P10 P59
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) C
Line_on (Li B C) A1 \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp)
[PROOF STEP]
have P60 : "Line_on (Li B C) A1 \<Longrightarrow> Line_on (Li B A) C"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B C) C
Line_on (Li B C) A1 \<Longrightarrow> Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B A)) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P32 P60
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) C
Line_on (Li B C) A1 \<Longrightarrow> Line_on (Li B A) C
[PROOF STEP]
have P61 : "\<not> Line_on (Li B C) A1"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) C
Line_on (Li B C) A1 \<Longrightarrow> Line_on (Li B A) C

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P7 P48
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B A1)) add Emp)
Line_on (Li B A1) A1
[PROOF STEP]
have "Line_on (Li B A) A1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B A1)) add Emp)
Line_on (Li B A1) A1

goal (1 subgoal):
 1. Line_on (Li B A) A1
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li B A) A1

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B A) A1
[PROOF STEP]
have P62 : "Eq (Geos (Poi A1) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Line_on (Li B A) D"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B A) A1

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P34 P62
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B A) D
Eq (Geos (Poi A1) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Line_on (Li B A) D
[PROOF STEP]
have P63 : "\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B A) D
Eq (Geos (Poi A1) add Emp) (Geos (Poi D) add Emp) \<Longrightarrow> Line_on (Li B A) D

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P36 P57 P61 P63
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B C) A1 D
\<not> Line_on (Li B C) A1
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have P64 : "\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow>
    Plane_sameside (Li B C) A1 D"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) D
\<not> Eq (Geos (Poi A) add Emp) (Geos (Poi A1) add Emp) \<Longrightarrow> \<not> Plane_diffside (Li B C) A1 D
\<not> Line_on (Li B C) A1
\<not> Eq (Geos (Poi A1) add Emp) (Geos (Poi D) add Emp)

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

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

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P12 P66
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B C1)) add Emp)
Plane_sameside (Li B C) A1 D
[PROOF STEP]
have P67 : "Plane_sameside (Li B C1) A1 D"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B C1)) add Emp)
Plane_sameside (Li B C) A1 D

goal (1 subgoal):
 1. Plane_sameside (Li B C1) A1 D
[PROOF STEP]
by (simp add:Plane_Line_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li B C1) A1 D

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P12
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B C1)) add Emp)
[PROOF STEP]
have P68 : "Line_on (Li B C1) A1 \<Longrightarrow> Line_on (Li B C) A1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li B C1)) add Emp)

goal (1 subgoal):
 1. Line_on (Li B C1) A1 \<Longrightarrow> Line_on (Li B C) A1
[PROOF STEP]
by (blast intro:Line_on_trans Eq_rev)
[PROOF STATE]
proof (state)
this:
Line_on (Li B C1) A1 \<Longrightarrow> Line_on (Li B C) A1

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P61 P68
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li B C) A1
Line_on (Li B C1) A1 \<Longrightarrow> Line_on (Li B C) A1
[PROOF STEP]
have P69 : "\<not> Line_on (Li B C1) A1"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li B C) A1
Line_on (Li B C1) A1 \<Longrightarrow> Line_on (Li B C) A1

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

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

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An B C1 A1))
[PROOF STEP]
have P70 : "Def (Ang (An A1 B C1))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An B C1 A1))

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

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
from P41 P67 P70
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B A1) C1 D
Plane_sameside (Li B C1) A1 D
Def (Ang (An A1 B C1))
[PROOF STEP]
show "Ang_inside (An A1 B C1) D"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B A1) C1 D
Plane_sameside (Li B C1) A1 D
Def (Ang (An A1 B C1))

goal (1 subgoal):
 1. Ang_inside (An A1 B C1) D
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An A1 B C1) D

goal:
No subgoals!
[PROOF STEP]
qed