[STATEMENT]
lemma (in Congruence_Rule) Ang_complementary_inside : 
  assumes 
    "Def (Ang (An p1 p2 p3))"
    "Bet_Point (Se p3 p4) p2"
    "Ang_inside (An p5 p2 p3) p1"
  shows 
    "Ang_inside (An p1 p2 p4) p5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P1 : "Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P2 : "Line_on (Li p2 p3) p4"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Line_on (Li p2 p3) p4
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p4

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P3 : "Line_on (Li p2 p3) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p3) p2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P4 : "Line_on (Li p2 p4) p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p4) p2
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p4) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P5 : "Line_on (Li p2 p4) p4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p4) p4
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p4) p4

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P6 : "\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

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

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

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P1 P7
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
Eq (Geos (Lin (Li p2 p3)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)
[PROOF STEP]
have P8 : "Plane_sameside (Li p2 p4) p5 p1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
Eq (Geos (Lin (Li p2 p3)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)

goal (1 subgoal):
 1. Plane_sameside (Li p2 p4) p5 p1
[PROOF STEP]
by (blast intro:Plane_Line_trans)
[PROOF STATE]
proof (state)
this:
Plane_sameside (Li p2 p4) p5 p1

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

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p1) p1
[PROOF STEP]
have P10 : "Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp) \<Longrightarrow>
    Line_on (Li p3 p4) p1"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p1) p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P1
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1
[PROOF STEP]
have P11 : "\<not> Line_on (Li p2 p3) p1"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p5) p3 p1 \<and> Plane_sameside (Li p2 p3) p5 p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P12 : "Line_on (Li p3 p4) p2"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Line_on (Li p3 p4) p2
[PROOF STEP]
by (simp add:Line_Bet_on)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p2

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P13 : "Line_on (Li p3 p4) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p3 p4) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p3 p4) p3

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
have P14 : "Line_on (Li p2 p3) p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Line_on (Li p2 p3) p3
[PROOF STEP]
by (simp add:Line_on_rule)
[PROOF STATE]
proof (state)
this:
Line_on (Li p2 p3) p3

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P15 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P3 P12 P13 P14 P15
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p3) p2
Line_on (Li p3 p4) p2
Line_on (Li p3 p4) p3
Line_on (Li p2 p3) p3
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)
[PROOF STEP]
have P16 : "Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p3)) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p3) p2
Line_on (Li p3 p4) p2
Line_on (Li p3 p4) p3
Line_on (Li p2 p3) p3
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)

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

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

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

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

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms P9 P18
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
Line_on (Li p2 p1) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp)
[PROOF STEP]
have P19 : "Plane_diffside (Li p2 p1) p3 p4"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
Line_on (Li p2 p1) p2
\<not> Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p1)) add Emp)

goal (1 subgoal):
 1. Plane_diffside (Li p2 p1) p3 p4
[PROOF STEP]
by (simp add:Plane_Bet_diffside)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p2 p1) p3 p4

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have P20 : "Plane_diffside (Li p2 p1) p3 p5"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

goal (1 subgoal):
 1. Plane_diffside (Li p2 p1) p3 p5
[PROOF STEP]
by (simp add:Ang_inside_Planeside Plane_diffside_rev)
[PROOF STATE]
proof (state)
this:
Plane_diffside (Li p2 p1) p3 p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P5
[PROOF STATE]
proof (chain)
picking this:
Line_on (Li p2 p4) p4
[PROOF STEP]
have P21 : "Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Line_on (Li p2 p4) p4

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p4) p5 p1
[PROOF STEP]
have P22 : "\<not> Line_on (Li p2 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p4) p5 p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P21 P22
[PROOF STATE]
proof (chain)
picking this:
Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5
\<not> Line_on (Li p2 p4) p5
[PROOF STEP]
have P23 : "\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp) \<Longrightarrow> Line_on (Li p2 p4) p5
\<not> Line_on (Li p2 p4) p5

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P19 P20 P23
[PROOF STATE]
proof (chain)
picking this:
Plane_diffside (Li p2 p1) p3 p4
Plane_diffside (Li p2 p1) p3 p5
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)
[PROOF STEP]
have P24 : "Plane_sameside (Li p2 p1) p4 p5"
[PROOF STATE]
proof (prove)
using this:
Plane_diffside (Li p2 p1) p3 p4
Plane_diffside (Li p2 p1) p3 p5
\<not> Eq (Geos (Poi p4) add Emp) (Geos (Poi p5) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p1) p4 p5
[PROOF STEP]
have P25 : "\<not> Line_on (Li p2 p1) p4"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p1) p4 p5

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1
[PROOF STEP]
have "\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p1 p2 p3))
Bet_Point (Se p3 p4) p2
Ang_inside (An p5 p2 p3) p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)
[PROOF STEP]
have P26 : "\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)"
[PROOF STATE]
proof (prove)
using this:
\<not> Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P25 P26
[PROOF STATE]
proof (chain)
picking this:
\<not> Line_on (Li p2 p1) p4
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)
[PROOF STEP]
have "Def (Ang (An p2 p1 p4))"
[PROOF STATE]
proof (prove)
using this:
\<not> Line_on (Li p2 p1) p4
\<not> Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)

goal (1 subgoal):
 1. Def (Ang (An p2 p1 p4))
[PROOF STEP]
by (simp add:Ang_sinple_def)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p2 p1 p4))

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Def (Ang (An p2 p1 p4))
[PROOF STEP]
have P27 : "Def (Ang (An p1 p2 p4))"
[PROOF STATE]
proof (prove)
using this:
Def (Ang (An p2 p1 p4))

goal (1 subgoal):
 1. Def (Ang (An p1 p2 p4))
[PROOF STEP]
by (blast intro:Ang_def_rev Ang_def_inv)
[PROOF STATE]
proof (state)
this:
Def (Ang (An p1 p2 p4))

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P8
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p4) p5 p1
[PROOF STEP]
have P28 : "Plane_sameside (Li p2 p4) p1 p5"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p4) p5 p1

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

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
from P24 P27 P28
[PROOF STATE]
proof (chain)
picking this:
Plane_sameside (Li p2 p1) p4 p5
Def (Ang (An p1 p2 p4))
Plane_sameside (Li p2 p4) p1 p5
[PROOF STEP]
show "Ang_inside (An p1 p2 p4) p5"
[PROOF STATE]
proof (prove)
using this:
Plane_sameside (Li p2 p1) p4 p5
Def (Ang (An p1 p2 p4))
Plane_sameside (Li p2 p4) p1 p5

goal (1 subgoal):
 1. Ang_inside (An p1 p2 p4) p5
[PROOF STEP]
by (simp add:Ang_inside_def)
[PROOF STATE]
proof (state)
this:
Ang_inside (An p1 p2 p4) p5

goal:
No subgoals!
[PROOF STEP]
qed