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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An A B C))
[PROOF STEP]
have P3 : "\<not> Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D
      \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
      \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An A B C))

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

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

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. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from assms P4
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
\<not> Line_on (Li B C) D
[PROOF STEP]
have "Def (Ang (An B C D))"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
\<not> Line_on (Li B C) D

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An D B C))
[PROOF STEP]
have P6 : "\<not> Ang_inside (An D B C) A \<Longrightarrow> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
      \<or> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
      \<or> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An D B C))

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P3 P6
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
\<not> Ang_inside (An D B C) A \<Longrightarrow> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
[PROOF STEP]
have P7 : "\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow>
    \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
    \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An A B C) D \<Longrightarrow> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D
\<not> Ang_inside (An D B C) A \<Longrightarrow> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
[PROOF STEP]
have P8 : "Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
    \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)

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

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

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. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B C) D A
[PROOF STEP]
have P9 : "\<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
    \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B C) D A

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P10 : "Line_on (Li C B) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C B) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C B) C

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P11 : "Line_on (Li C B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C B) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C B) B

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P21 : "Line_on (Li E C) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li E C) C
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li E C) C

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from assms P13 P16 P17 P21
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
Line_on (Li E C) B
Line_on (Li B C) B
Line_on (Li B C) C
Line_on (Li E C) C
[PROOF STEP]
have P22 : "Eq (Geos (Lin (Li E C)) add Emp) (Geos (Lin (Li B C)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li B C) A D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)
\<not> Eq (Geos (Lin (Li B A)) add Emp) (Geos (Lin (Li B D)) add Emp)
Line_on (Li E C) B
Line_on (Li B C) B
Line_on (Li B C) C
Line_on (Li E C) C

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P26 : "Line_on (Li E C) E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li E C) E
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li E C) E

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P32 : "Line_on (Li B D) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D) B
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) B

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P29
[PROOF STATE]
proof (chain)
picking this:
Bet_Point (Se C E) B
[PROOF STEP]
have P37 : "Bet_Point (Se E C) B"
[PROOF STATE]
proof (prove)
using this:
Bet_Point (Se C E) B

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P46 : "Plane_diffside (Li B D) C A \<Longrightarrow> \<not> Plane_sameside (Li B D) C A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plane_diffside (Li B D) C A \<Longrightarrow> \<not> Plane_sameside (Li B D) C A
[PROOF STEP]
by (simp add:Plane_diffside_not_sameside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li B D) C A \<Longrightarrow> \<not> Plane_sameside (Li B D) C A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P56 : "Line_on (Li B D) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li B D) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li B D) D

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P16
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B C) B
[PROOF STEP]
have P57 : "Eq (Geos (Poi B) 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) B

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P32 P48 P53 P55 P56 P58
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) B
Plane_diffside (Li B D) C A \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se C A) F
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp)
Plane_diffside (Li B D) C A \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B D) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
[PROOF STEP]
have "\<not> Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) C A \<Longrightarrow>
    Bet_Point (Se B F) D \<or> Bet_Point (Se F D) B \<or> Bet_Point (Se D B) F"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) B
Plane_diffside (Li B D) C A \<Longrightarrow> Line_on (Li B D) F \<and> Bet_Point (Se C A) F
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp)
Plane_diffside (Li B D) C A \<Longrightarrow> \<not> Eq (Geos (Poi F) add Emp) (Geos (Poi B) add Emp)
Line_on (Li B D) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)

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

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

goal (1 subgoal):
 1. \<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F
[PROOF STEP]
by (simp add:Bet_case_fact)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have P63 : "Line_on (Li F D) D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li F D) D
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li F D) D

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P32 P56 P58 P62 P63
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li B D) B
Line_on (Li B D) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Bet_Point (Se F D) B \<Longrightarrow> Line_on (Li F D) B
Line_on (Li F D) D
[PROOF STEP]
have P64 : "Bet_Point (Se F D) B \<Longrightarrow> Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li B D)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li B D) B
Line_on (Li B D) D
\<not> Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)
Bet_Point (Se F D) B \<Longrightarrow> Line_on (Li F D) B
Line_on (Li F D) D

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
have "Line_on (Li C A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li C A) A
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li C A) A

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P59
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F
[PROOF STEP]
have P75 : "\<not> Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) C A \<Longrightarrow>
    Bet_Point (Se B F) D \<Longrightarrow> \<not> Bet_Point (Se D F) B"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F

goal (1 subgoal):
 1. \<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A; Bet_Point (Se B F) D\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D F) B
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A; Bet_Point (Se B F) D\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D F) B

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se B F) D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se B F) D

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P59
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F
[PROOF STEP]
have P78 : "\<not> Ang_inside (An A B C) D \<Longrightarrow> Plane_diffside (Li B D) C A \<Longrightarrow>
    Bet_Point (Se D B) F \<Longrightarrow> \<not> Bet_Point (Se D F) B"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F

goal (1 subgoal):
 1. \<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A; Bet_Point (Se D B) F\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D F) B
[PROOF STEP]
by (blast intro:Bet_rev)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A; Bet_Point (Se D B) F\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D F) B

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D B) F
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D B) F

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P59 P73 P76 P79
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F
Plane_sameside (Li B C) A D \<and> Plane_diffside (Li B D) C A \<Longrightarrow> \<not> Bet_Point (Se F D) B
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se B F) D
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D B) F
[PROOF STEP]
have "\<not> Ang_inside (An A B C) D \<and> Plane_sameside (Li B C) A D \<and> Plane_diffside (Li B D) C A \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> Bet_Point (Se F D) B \<and> \<not> Bet_Point (Se D B) F \<or> \<not> Bet_Point (Se B F) D \<and> \<not> Bet_Point (Se F D) B \<and> Bet_Point (Se D B) F
Plane_sameside (Li B C) A D \<and> Plane_diffside (Li B D) C A \<Longrightarrow> \<not> Bet_Point (Se F D) B
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se B F) D
\<lbrakk>\<not> Ang_inside (An A B C) D; Plane_diffside (Li B D) C A\<rbrakk> \<Longrightarrow> \<not> Bet_Point (Se D B) F

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

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

goal (1 subgoal):
 1. \<not> Ang_inside (An A B C) D \<and> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_diffside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<Longrightarrow> False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> Ang_inside (An A B C) D \<and> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_diffside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An D B C))
[PROOF STEP]
have "Def (Tri (Tr B D C))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An D B C))

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Tri (Tr B D C))
[PROOF STEP]
have P81 : "\<not> Line_on (Li B D) C"
[PROOF STATE]
proof (prove)
using this:
Def (Tri (Tr B D C))

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P80 P84
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An A B C) D \<and> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_diffside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<Longrightarrow> False
\<not> Plane_sameside (Li B D) C A \<Longrightarrow> Plane_diffside (Li B D) C A
[PROOF STEP]
have P85 : "\<not> Ang_inside (An A B C) D \<and> \<not> Plane_sameside (Li B A) C D
    \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An A B C) D \<and> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_diffside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<Longrightarrow> False
\<not> Plane_sameside (Li B D) C A \<Longrightarrow> Plane_diffside (Li B D) C A

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

goal (1 subgoal):
 1. \<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)
[PROOF STEP]
from P7 P8 P9 P85
[PROOF STATE]
proof (chain)
picking this:
\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<Longrightarrow> False
\<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<Longrightarrow> False
\<not> Ang_inside (An A B C) D \<and> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<Longrightarrow> False
[PROOF STEP]
show "\<not> (\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A)"
[PROOF STATE]
proof (prove)
using this:
\<not> Ang_inside (An A B C) D \<and> \<not> Ang_inside (An D B C) A \<Longrightarrow> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A
Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> \<not> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<Longrightarrow> False
\<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<or> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> \<not> Plane_sameside (Li B C) D A \<Longrightarrow> False
\<not> Ang_inside (An A B C) D \<and> \<not> Plane_sameside (Li B A) C D \<and> Plane_sameside (Li B C) A D \<and> \<not> Plane_sameside (Li B D) C A \<and> Plane_sameside (Li B C) D A \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed