[STATEMENT]
lemma (in Congruence_Rule) Planeside_wrong_relation :
  assumes
    "Plane_diffside (Li p1 p2) p3 p4"
    "Plane_diffside (Li p1 p3) p2 p4"
    "Plane_sameside (Li p1 p5) p3 p2"
    "Plane_sameside (Li p1 p5) p4 p2"
  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]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2
[PROOF STEP]
have "\<exists>p. Bet_Point (Se p3 p4) p \<and> Line_on (Li p1 p2) p
    \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se p3 p4) p \<and> Line_on (Li p1 p2) p \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se p3 p4) p \<and> Line_on (Li p1 p2) p \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se p3 p4) p \<and> Line_on (Li p1 p2) p \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
[PROOF STEP]
obtain p6 :: Point where P1 : "Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6
    \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se p3 p4) p \<and> Line_on (Li p1 p2) p \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. (\<And>p6. Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2
[PROOF STEP]
have "\<exists>p. Bet_Point (Se p2 p4) p \<and> Line_on (Li p1 p3) p
    \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2

goal (1 subgoal):
 1. \<exists>p. Bet_Point (Se p2 p4) p \<and> Line_on (Li p1 p3) p \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
[PROOF STEP]
by (simp add:Plane_diffside_def)
[PROOF STATE]
proof (state)
this:
\<exists>p. Bet_Point (Se p2 p4) p \<and> Line_on (Li p1 p3) p \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Bet_Point (Se p2 p4) p \<and> Line_on (Li p1 p3) p \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
[PROOF STEP]
obtain p7 :: Point where P2 : "Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7
    \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Bet_Point (Se p2 p4) p \<and> Line_on (Li p1 p3) p \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4

goal (1 subgoal):
 1. (\<And>p7. Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
[PROOF STEP]
have P3 : "Bet_Point (Se p2 p4) p7"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4

goal (1 subgoal):
 1. Bet_Point (Se p2 p4) p7
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p2 p4) p7

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7
[PROOF STEP]
have P4 : "Line_on (Li p2 p4) p7"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7

goal (1 subgoal):
 1. Line_on (Li p2 p4) p7
[PROOF STEP]
by (blast intro:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p4) p7

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

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P4 P5 P6 P7
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p4) p7
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p7) add Emp)
Line_on (Li p2 p4) p4
Line_on (Li p3 p4) p4
[PROOF STEP]
have P8 : "Line_on (Li p3 p4) p7 \<Longrightarrow>
    Eq (Geos (Lin (Li p2 p4)) add Emp) (Geos (Lin (Li p3 p4)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p4) p7
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p7) add Emp)
Line_on (Li p2 p4) p4
Line_on (Li p3 p4) p4

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

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

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

goal (1 subgoal):
 1. Line_on (Li p3 p4) p7 \<Longrightarrow> Line_on (Li p3 p4) p2
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p7 \<Longrightarrow> Line_on (Li p3 p4) p2

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

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
[PROOF STEP]
have P13 : "Bet_Point (Se p3 p4) p6"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. Bet_Point (Se p3 p4) p6
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p3 p4) p6

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6
[PROOF STEP]
have P14 : "Line_on (Li p3 p4) p6"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6

goal (1 subgoal):
 1. Line_on (Li p3 p4) p6
[PROOF STEP]
by (blast intro:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p6

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1 P10 P12 P14 P15
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Line_on (Li p3 p4) p7 \<Longrightarrow> Line_on (Li p3 p4) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
Line_on (Li p3 p4) p6
Line_on (Li p1 p2) p2
[PROOF STEP]
have P16 : "Line_on (Li p3 p4) p7 \<Longrightarrow>
    Eq (Geos (Poi p6) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Line_on (Li p3 p4) p7 \<Longrightarrow> Line_on (Li p3 p4) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
Line_on (Li p3 p4) p6
Line_on (Li p1 p2) p2

goal (1 subgoal):
 1. Line_on (Li p3 p4) p7 \<Longrightarrow> Eq (Geos (Poi p6) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
by (simp add:Line_unique_Point)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p7 \<Longrightarrow> Eq (Geos (Poi p6) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P13 P16
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6
Line_on (Li p3 p4) p7 \<Longrightarrow> Eq (Geos (Poi p6) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P17 : "Line_on (Li p3 p4) p7 \<Longrightarrow> Bet_Point (Se p3 p4) p2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6
Line_on (Li p3 p4) p7 \<Longrightarrow> Eq (Geos (Poi p6) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. Line_on (Li p3 p4) p7 \<Longrightarrow> Bet_Point (Se p3 p4) p2
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p7 \<Longrightarrow> Bet_Point (Se p3 p4) p2

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P2 P18
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p1 p3)) add Emp) \<Longrightarrow> Line_on (Li p1 p3) p4
[PROOF STEP]
have P19 : "\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p1 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p1 p3)) add Emp) \<Longrightarrow> Line_on (Li p1 p3) p4

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P17 P19 P20
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p4) p7 \<Longrightarrow> Bet_Point (Se p3 p4) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p1 p3)) add Emp)
Line_on (Li p1 p3) p3
[PROOF STEP]
have "Line_on (Li p3 p4) p7 \<Longrightarrow> Plane_sameside (Li p1 p3) p2 p4"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p4) p7 \<Longrightarrow> Bet_Point (Se p3 p4) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p1 p3)) add Emp)
Line_on (Li p1 p3) p3

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

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p4) p7 \<Longrightarrow> Plane_sameside (Li p1 p3) p2 p4
[PROOF STEP]
have "Line_on (Li p3 p4) p7 \<Longrightarrow> \<not> Plane_diffside (Li p1 p3) p2 p4"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p4) p7 \<Longrightarrow> Plane_sameside (Li p1 p3) p2 p4

goal (1 subgoal):
 1. Line_on (Li p3 p4) p7 \<Longrightarrow> \<not> Plane_diffside (Li p1 p3) p2 p4
[PROOF STEP]
by (simp add:Plane_sameside_not_diffside)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p7 \<Longrightarrow> \<not> Plane_diffside (Li p1 p3) p2 p4

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p4) p7 \<Longrightarrow> \<not> Plane_diffside (Li p1 p3) p2 p4
[PROOF STEP]
have P21 : "\<not> Line_on (Li p3 p4) p7"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p4) p7 \<Longrightarrow> \<not> Plane_diffside (Li p1 p3) p2 p4

goal (1 subgoal):
 1. \<not> Line_on (Li p3 p4) p7
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p4) p7 \<Longrightarrow> \<not> Plane_diffside (Li p1 p3) p2 p4
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2

goal (1 subgoal):
 1. \<not> Line_on (Li p3 p4) p7
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p3 p4) p7

goal (1 subgoal):
 1. False
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7
[PROOF STEP]
have P22 : "\<not> Eq (Geos (Poi p7) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P4 P9 P15 P22
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p4) p7
Line_on (Li p2 p4) p2
Line_on (Li p1 p2) p2
\<not> Eq (Geos (Poi p7) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P23 : "Line_on (Li p1 p2) p7 \<Longrightarrow>
    Eq (Geos (Lin (Li p2 p4)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p4) p7
Line_on (Li p2 p4) p2
Line_on (Li p1 p2) p2
\<not> Eq (Geos (Poi p7) add Emp) (Geos (Poi p2) add Emp)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P6 P23
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p4) p4
Line_on (Li p1 p2) p7 \<Longrightarrow> Eq (Geos (Lin (Li p2 p4)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
[PROOF STEP]
have P24 : "Line_on (Li p1 p2) p7 \<Longrightarrow> Line_on (Li p1 p2) p4"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p4) p4
Line_on (Li p1 p2) p7 \<Longrightarrow> Eq (Geos (Lin (Li p2 p4)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)

goal (1 subgoal):
 1. Line_on (Li p1 p2) p7 \<Longrightarrow> Line_on (Li p1 p2) p4
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p2) p7 \<Longrightarrow> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1 P24
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Line_on (Li p1 p2) p7 \<Longrightarrow> Line_on (Li p1 p2) p4
[PROOF STEP]
have P25 : "\<not> Line_on (Li p1 p2) p7"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Line_on (Li p1 p2) p7 \<Longrightarrow> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. \<not> Line_on (Li p1 p2) p7
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p1 p2) p7

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1 P13 P21 P25
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Bet_Point (Se p3 p4) p6
\<not> Line_on (Li p3 p4) p7
\<not> Line_on (Li p1 p2) p7
[PROOF STEP]
have P26 : "Line_on_Seg (Li p1 p2) (Se p3 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p4 p7)
        \<or> Line_on_Seg (Li p1 p2) (Se p4 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p3 p7)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Bet_Point (Se p3 p4) p6
\<not> Line_on (Li p3 p4) p7
\<not> Line_on (Li p1 p2) p7

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p2) (Se p3 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p4 p7) \<or> Line_on_Seg (Li p1 p2) (Se p4 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p3 p7)
[PROOF STEP]
by (simp add:Pachets_axiom)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p3 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p4 p7) \<or> Line_on_Seg (Li p1 p2) (Se p4 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p3 p7)

goal (1 subgoal):
 1. False
[PROOF STEP]
have "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p4 p7) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p4 p7) p
[PROOF STEP]
by (simp add:Line_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p4 p7) p

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p4 p7) p
[PROOF STEP]
obtain p8 :: Point where P27 : "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow>
    Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p4 p7) p

goal (1 subgoal):
 1. (\<And>p8. (Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8
[PROOF STEP]
have P28 : "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p4 p7) p8"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p4 p7) p8
[PROOF STEP]
by (blast intro:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p4 p7) p8

goal (1 subgoal):
 1. False
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7
[PROOF STEP]
have P29 : "Line_on (Li p4 p7) p2"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7

goal (1 subgoal):
 1. Line_on (Li p4 p7) p2
[PROOF STEP]
by (blast intro:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p4 p7) p2

goal (1 subgoal):
 1. False
[PROOF STEP]
from P27
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8
[PROOF STEP]
have "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Bet_Point (Se p4 p7) p8"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Bet_Point (Se p4 p7) p8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Bet_Point (Se p4 p7) p8

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Bet_Point (Se p4 p7) p8
[PROOF STEP]
have P30 : "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow>
    Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp) \<Longrightarrow> Bet_Point (Se p4 p7) p2"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Bet_Point (Se p4 p7) p8

goal (1 subgoal):
 1. \<lbrakk>Line_on_Seg (Li p1 p2) (Se p4 p7); Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se p4 p7) p2
[PROOF STEP]
by (simp add:Point_Eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Line_on_Seg (Li p1 p2) (Se p4 p7); Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se p4 p7) p2

goal (1 subgoal):
 1. False
[PROOF STEP]
from P3
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7
[PROOF STEP]
have "Inv (Bet_Point (Se p4 p7) p2)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7

goal (1 subgoal):
 1. Inv (Bet_Point (Se p4 p7) p2)
[PROOF STEP]
by (simp add:Bet_iff)
[PROOF STATE]
proof (state)
this:
Inv (Bet_Point (Se p4 p7) p2)

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inv (Bet_Point (Se p4 p7) p2)
[PROOF STEP]
have P31 : "\<not> Bet_Point (Se p4 p7) p2"
[PROOF STATE]
proof (prove)
using this:
Inv (Bet_Point (Se p4 p7) p2)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P30 P31
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Line_on_Seg (Li p1 p2) (Se p4 p7); Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se p4 p7) p2
\<not> Bet_Point (Se p4 p7) p2
[PROOF STEP]
have P32 : "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow>
    \<not> Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Line_on_Seg (Li p1 p2) (Se p4 p7); Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)\<rbrakk> \<Longrightarrow> Bet_Point (Se p4 p7) p2
\<not> Bet_Point (Se p4 p7) p2

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<not> Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<not> Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P15 P27 P28 P29 P32
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p2) p2
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p4 p7) p8
Line_on (Li p4 p7) p2
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<not> Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P33 : "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow>
    Eq (Geos (Lin (Li p4 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p2) p2
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p4 p7) p8
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p4 p7) p8
Line_on (Li p4 p7) p2
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> \<not> Eq (Geos (Poi p8) add Emp) (Geos (Poi p2) add Emp)

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P33 P34
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Eq (Geos (Lin (Li p4 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
Line_on (Li p4 p7) p4
[PROOF STEP]
have P35 : "Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p4"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Eq (Geos (Lin (Li p4 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
Line_on (Li p4 p7) p4

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p4
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1 P35
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p4
[PROOF STEP]
have P36 : "\<not> Line_on_Seg (Li p1 p2) (Se p4 p7)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Line_on_Seg (Li p1 p2) (Se p4 p7) \<Longrightarrow> Line_on (Li p1 p2) p4

goal (1 subgoal):
 1. \<not> Line_on_Seg (Li p1 p2) (Se p4 p7)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on_Seg (Li p1 p2) (Se p4 p7)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P26 P36
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p2) (Se p3 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p4 p7) \<or> Line_on_Seg (Li p1 p2) (Se p4 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p3 p7)
\<not> Line_on_Seg (Li p1 p2) (Se p4 p7)
[PROOF STEP]
have "Line_on_Seg (Li p1 p2) (Se p3 p7)"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p2) (Se p3 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p4 p7) \<or> Line_on_Seg (Li p1 p2) (Se p4 p7) \<and> \<not> Line_on_Seg (Li p1 p2) (Se p3 p7)
\<not> Line_on_Seg (Li p1 p2) (Se p4 p7)

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p2) (Se p3 p7)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p2) (Se p3 p7)

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p2) (Se p3 p7)
[PROOF STEP]
have "\<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p3 p7) p"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p2) (Se p3 p7)

goal (1 subgoal):
 1. \<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p3 p7) p
[PROOF STEP]
by (simp add:Line_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
\<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p3 p7) p

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p3 p7) p
[PROOF STEP]
obtain p8 :: Point where P37 : "Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Line_on (Li p1 p2) p \<and> Bet_Point (Se p3 p7) p

goal (1 subgoal):
 1. (\<And>p8. Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8

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

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p4) p3
[PROOF STEP]
have P38 : "Eq (Geos (Poi p3) add Emp) (Geos (Poi p7) add Emp) \<Longrightarrow> Line_on (Li p3 p4) p7"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p4) p3

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P21 P38
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p3 p4) p7
Eq (Geos (Poi p3) add Emp) (Geos (Poi p7) add Emp) \<Longrightarrow> Line_on (Li p3 p4) p7
[PROOF STEP]
have P39 : "\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p7) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p3 p4) p7
Eq (Geos (Poi p3) add Emp) (Geos (Poi p7) add Emp) \<Longrightarrow> Line_on (Li p3 p4) p7

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P2
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
[PROOF STEP]
have P42 : "Line_on (Li p1 p3) p7"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4

goal (1 subgoal):
 1. Line_on (Li p1 p3) p7
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p3) p7

goal (1 subgoal):
 1. False
[PROOF STEP]
from P20 P39 P40 P41 P42
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p3) p3
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p7) add Emp)
Line_on (Li p3 p7) p3
Line_on (Li p3 p7) p7
Line_on (Li p1 p3) p7
[PROOF STEP]
have P43 :
    "Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p3 p7)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p3) p3
\<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p7) add Emp)
Line_on (Li p3 p7) p3
Line_on (Li p3 p7) p7
Line_on (Li p1 p3) p7

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P43 P44
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p3 p7)) add Emp)
Line_on (Li p1 p3) p1
[PROOF STEP]
have P45 : "Line_on (Li p3 p7) p1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p3 p7)) add Emp)
Line_on (Li p1 p3) p1

goal (1 subgoal):
 1. Line_on (Li p3 p7) p1
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p7) p1

goal (1 subgoal):
 1. False
[PROOF STEP]
from P37
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8
[PROOF STEP]
have P46 : "Line_on (Li p3 p7) p8"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8

goal (1 subgoal):
 1. Line_on (Li p3 p7) p8
[PROOF STEP]
by (blast intro:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p7) p8

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P40
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p7) p3
[PROOF STEP]
have P48 : "Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp) \<Longrightarrow>
    Line_on (Li p1 p2) p3"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p7) p3

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P1 P48
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp) \<Longrightarrow> Line_on (Li p1 p2) p3
[PROOF STEP]
have P49 : "\<not> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p4) p6 \<and> Line_on (Li p1 p2) p6 \<and> \<not> Line_on (Li p1 p2) p3 \<and> \<not> Line_on (Li p1 p2) p4
Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp) \<Longrightarrow> Line_on (Li p1 p2) p3

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P37 P45 P46 P48 P47 P49
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8
Line_on (Li p3 p7) p1
Line_on (Li p3 p7) p8
Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp) \<Longrightarrow> Line_on (Li p1 p2) p3
Line_on (Li p1 p2) p1
\<not> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
[PROOF STEP]
have P50 : "Eq (Geos (Poi p8) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8
Line_on (Li p3 p7) p1
Line_on (Li p3 p7) p8
Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp) \<Longrightarrow> Line_on (Li p1 p2) p3
Line_on (Li p1 p2) p1
\<not> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)

goal (1 subgoal):
 1. Eq (Geos (Poi p8) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
by (simp add:Line_unique_Point)
[PROOF STATE]
proof (state)
this:
Eq (Geos (Poi p8) add Emp) (Geos (Poi p1) add Emp)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P37
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8
[PROOF STEP]
have P51 : "Bet_Point (Se p3 p7) p8"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p2) p8 \<and> Bet_Point (Se p3 p7) p8

goal (1 subgoal):
 1. Bet_Point (Se p3 p7) p8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p3 p7) p8

goal (1 subgoal):
 1. False
[PROOF STEP]
from P50 P51
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi p8) add Emp) (Geos (Poi p1) add Emp)
Bet_Point (Se p3 p7) p8
[PROOF STEP]
have P52 : "Bet_Point (Se p3 p7) p1"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi p8) add Emp) (Geos (Poi p1) add Emp)
Bet_Point (Se p3 p7) p8

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P44
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p3) p1
[PROOF STEP]
have P53 : "Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp) \<Longrightarrow> Line_on (Li p1 p3) p2"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p3) p1

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P2 P53
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp) \<Longrightarrow> Line_on (Li p1 p3) p2
[PROOF STEP]
have P54 : "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7 \<and> Line_on (Li p1 p3) p7 \<and> \<not> Line_on (Li p1 p3) p2 \<and> \<not> Line_on (Li p1 p3) p4
Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp) \<Longrightarrow> Line_on (Li p1 p3) p2

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P45 P47 P54 P55
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p7) p1
Line_on (Li p1 p2) p1
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Line_on (Li p1 p2) p2
[PROOF STEP]
have P56 : "Line_on (Li p3 p7) p2 \<Longrightarrow>
    Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p7) p1
Line_on (Li p1 p2) p1
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
Line_on (Li p1 p2) p2

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P49 P56
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
Line_on (Li p3 p7) p2 \<Longrightarrow> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
[PROOF STEP]
have P57 : "\<not> Line_on (Li p3 p7) p2"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)
Line_on (Li p3 p7) p2 \<Longrightarrow> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p3 p7) p2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p3 p7) p2

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2
[PROOF STEP]
have P58 : "\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3
    \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2

goal (1 subgoal):
 1. \<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P52
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p7) p1
[PROOF STEP]
have P59 : "\<not> Eq (Geos (Poi p7) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p7) p1

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P41 P45 P59 P60
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p7) p7
Line_on (Li p3 p7) p1
\<not> Eq (Geos (Poi p7) add Emp) (Geos (Poi p1) add Emp)
Line_on (Li p1 p5) p1
[PROOF STEP]
have P61 : "Line_on (Li p1 p5) p7 \<Longrightarrow>
    Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p5)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p7) p7
Line_on (Li p3 p7) p1
\<not> Eq (Geos (Poi p7) add Emp) (Geos (Poi p1) add Emp)
Line_on (Li p1 p5) p1

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P40 P61
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p3 p7) p3
Line_on (Li p1 p5) p7 \<Longrightarrow> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p5)) add Emp)
[PROOF STEP]
have P62 : "Line_on (Li p1 p5) p7 \<Longrightarrow> Line_on (Li p1 p5) p3"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p3 p7) p3
Line_on (Li p1 p5) p7 \<Longrightarrow> Eq (Geos (Lin (Li p3 p7)) add Emp) (Geos (Lin (Li p1 p5)) add Emp)

goal (1 subgoal):
 1. Line_on (Li p1 p5) p7 \<Longrightarrow> Line_on (Li p1 p5) p3
[PROOF STEP]
by (simp add:Line_on_trans)
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p5) p7 \<Longrightarrow> Line_on (Li p1 p5) p3

goal (1 subgoal):
 1. False
[PROOF STEP]
from P58 P62
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)
Line_on (Li p1 p5) p7 \<Longrightarrow> Line_on (Li p1 p5) p3
[PROOF STEP]
have P63 : "\<not> Line_on (Li p1 p5) p7"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)
Line_on (Li p1 p5) p7 \<Longrightarrow> Line_on (Li p1 p5) p3

goal (1 subgoal):
 1. \<not> Line_on (Li p1 p5) p7
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p1 p5) p7

goal (1 subgoal):
 1. False
[PROOF STEP]
from P58
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P64 : "\<not> Line_on (Li p1 p5) p3"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p1 p5) p3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p1 p5) p3

goal (1 subgoal):
 1. False
[PROOF STEP]
from P58
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P65 : "\<not> Line_on (Li p1 p5) p2"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)

goal (1 subgoal):
 1. \<not> Line_on (Li p1 p5) p2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> Line_on (Li p1 p5) p2

goal (1 subgoal):
 1. False
[PROOF STEP]
from P52 P57 P60 P63 P64 P65
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p3 p7) p1
\<not> Line_on (Li p3 p7) p2
Line_on (Li p1 p5) p1
\<not> Line_on (Li p1 p5) p7
\<not> Line_on (Li p1 p5) p3
\<not> Line_on (Li p1 p5) p2
[PROOF STEP]
have P66 : "Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p7 p2)
        \<or> Line_on_Seg (Li p1 p5) (Se p7 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p3 p2)"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p3 p7) p1
\<not> Line_on (Li p3 p7) p2
Line_on (Li p1 p5) p1
\<not> Line_on (Li p1 p5) p7
\<not> Line_on (Li p1 p5) p3
\<not> Line_on (Li p1 p5) p2

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p7 p2) \<or> Line_on_Seg (Li p1 p5) (Se p7 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p3 p2)
[PROOF STEP]
by (simp add:Pachets_axiom)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p7 p2) \<or> Line_on_Seg (Li p1 p5) (Se p7 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p3 p2)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P58 P66
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)
Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p7 p2) \<or> Line_on_Seg (Li p1 p5) (Se p7 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p3 p2)
[PROOF STEP]
have "Line_on_Seg (Li p1 p5) (Se p7 p2)"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on (Li p1 p5) p3 \<and> \<not> Line_on (Li p1 p5) p2 \<and> \<not> Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)
Line_on_Seg (Li p1 p5) (Se p3 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p7 p2) \<or> Line_on_Seg (Li p1 p5) (Se p7 p2) \<and> \<not> Line_on_Seg (Li p1 p5) (Se p3 p2)

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p5) (Se p7 p2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p5) (Se p7 p2)

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p5) (Se p7 p2)
[PROOF STEP]
have "\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p7 p2) p"
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p5) (Se p7 p2)

goal (1 subgoal):
 1. \<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p7 p2) p
[PROOF STEP]
by (simp add:Line_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p7 p2) p

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p7 p2) p
[PROOF STEP]
obtain p9 :: Point where P67 : "Line_on (Li p1 p5) p9 \<and> Bet_Point (Se p7 p2) p9"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p7 p2) p

goal (1 subgoal):
 1. (\<And>p9. Line_on (Li p1 p5) p9 \<and> Bet_Point (Se p7 p2) p9 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Line_on (Li p1 p5) p9 \<and> Bet_Point (Se p7 p2) p9

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p5) p9 \<and> Bet_Point (Se p7 p2) p9
[PROOF STEP]
have P68 : "Bet_Point (Se p2 p7) p9"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p5) p9 \<and> Bet_Point (Se p7 p2) p9

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P3 P68
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p7
Bet_Point (Se p2 p7) p9
[PROOF STEP]
have "Bet_Point (Se p2 p4) p9"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p7
Bet_Point (Se p2 p7) p9

goal (1 subgoal):
 1. Bet_Point (Se p2 p4) p9
[PROOF STEP]
by (blast intro:Bet_swap_134_124)
[PROOF STATE]
proof (state)
this:
Bet_Point (Se p2 p4) p9

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se p2 p4) p9
[PROOF STEP]
have P69 : "Bet_Point (Se p4 p2) p9"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se p2 p4) p9

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

goal (1 subgoal):
 1. False
[PROOF STEP]
from P67 P69
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p1 p5) p9 \<and> Bet_Point (Se p7 p2) p9
Bet_Point (Se p4 p2) p9
[PROOF STEP]
have "\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p4 p2) p"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p1 p5) p9 \<and> Bet_Point (Se p7 p2) p9
Bet_Point (Se p4 p2) p9

goal (1 subgoal):
 1. \<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p4 p2) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p4 p2) p

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p4 p2) p
[PROOF STEP]
have P70 : "Line_on_Seg (Li p1 p5) (Se p4 p2)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. Line_on (Li p1 p5) p \<and> Bet_Point (Se p4 p2) p

goal (1 subgoal):
 1. Line_on_Seg (Li p1 p5) (Se p4 p2)
[PROOF STEP]
by (simp add:Line_on_Seg_rule)
[PROOF STATE]
proof (state)
this:
Line_on_Seg (Li p1 p5) (Se p4 p2)

goal (1 subgoal):
 1. False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2
[PROOF STEP]
have P71 : "\<not> Line_on_Seg (Li p1 p5) (Se p4 p2)"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li p1 p2) p3 p4
Plane_diffside (Li p1 p3) p2 p4
Plane_sameside (Li p1 p5) p3 p2
Plane_sameside (Li p1 p5) p4 p2

goal (1 subgoal):
 1. \<not> Line_on_Seg (Li p1 p5) (Se p4 p2)
[PROOF STEP]
by (simp add:Plane_sameside_def)
[PROOF STATE]
proof (state)
this:
\<not> Line_on_Seg (Li p1 p5) (Se p4 p2)

goal (1 subgoal):
 1. False
[PROOF STEP]
from P70 P71
[PROOF STATE]
proof (chain)
picking this:
Line_on_Seg (Li p1 p5) (Se p4 p2)
\<not> Line_on_Seg (Li p1 p5) (Se p4 p2)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Line_on_Seg (Li p1 p5) (Se p4 p2)
\<not> Line_on_Seg (Li p1 p5) (Se p4 p2)

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

goal:
No subgoals!
[PROOF STEP]
qed