Theory Order

(*<*)
theory Order imports Incidence begin
(*>*)

section‹Order›

locale Definition_2 = Incidence_Rule +
  fixes Line_on_Seg :: "Line ⇒ Segment ⇒ bool"
    and Bet_Point :: "Segment ⇒ Point ⇒ bool"
    and Seg_on_Seg :: "Segment ⇒ Segment ⇒ bool"
    and Line_on_Line :: "Line ⇒ Line ⇒ bool"
    and Plane_sameside :: "Line ⇒ Point ⇒ Point ⇒ bool"
    and Plane_diffside :: "Line ⇒ Point ⇒ Point ⇒ bool"
  assumes Bet_Point_def : "⟦Bet_Point (Se p1 p2) p3⟧ ⟹ ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp) 
        ∧ ¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp) ∧ ¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)"
    and Bet_rev : "⟦Bet_Point (Se p1 p2) p3⟧ ⟹ Bet_Point (Se p2 p1) p3"
    and Line_Bet_exist : "⟦Bet_Point (Se p1 p2) p3⟧ ⟹ ∃l. Line_on l p1 ∧ Line_on l p2 ∧ Line_on l p3"
    and Seg_rev : "Eq (Geos (Seg (Se p1 p2)) add Emp) (Geos (Seg (Se p2 p1)) add Emp)"
    and Plane_sameside_def : "Plane_sameside l1 p1 p2 ⟷ ¬ Line_on_Seg l1 (Se p1 p2) ∧ ¬ Line_on l1 p1 ∧ ¬ Line_on l1 p2 ∧ ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
    and Plane_diffside_def : "Plane_diffside l1 p1 p2 ⟷ (∃p. Bet_Point (Se p1 p2) p ∧ Line_on l1 p ∧ ¬ Line_on l1 p1 ∧ ¬ Line_on l1 p2)"
        
locale Axiom_2 = Definition_2 +
  assumes Bet_extension : "⟦Line_on l1 p1; Line_on l1 p2; ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)⟧ ⟹ ∃p. Bet_Point (Se p1 p) p2 ∧ Line_on l1 p"
    and Bet_iff : "⟦Bet_Point (Se p1 p2) p3⟧ ⟹ Inv (Bet_Point (Se p2 p3) p1) ∧ Inv (Bet_Point (Se p3 p1) p2)"
    and Pachets_axiom : "⟦¬ Line_on (Li p1 p2) p3; Bet_Point (Se p1 p2) p4; Line_on l1 p4;
        ¬ Line_on l1 p1; ¬ Line_on l1 p2; ¬ Line_on l1 p3⟧ ⟹ 
        Line_on_Seg l1 (Se p1 p3) ∧ ¬ Line_on_Seg l1 (Se p2 p3)
        ∨ Line_on_Seg l1 (Se p2 p3) ∧ ¬ Line_on_Seg l1 (Se p1 p3)"
    and Seg_move_sameside : "⟦Line_on l1 p1; Line_on l1 p2; ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp);
        ¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)⟧ ⟹ 
        ∃p. Eq (Geos (Seg (Se p3 p4)) add Emp) (Geos (Seg (Se p1 p)) add Emp) ∧ ¬ Bet_Point (Se p p2) p1 ∧ Line_on l1 p ∧ ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p) add Emp)"
    and Seg_move_diffside : "⟦Line_on l1 p1; Line_on l1 p2; ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp);
        ¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)⟧ ⟹ 
        ∃p. Eq (Geos (Seg (Se p3 p4)) add Emp) (Geos (Seg (Se p1 p)) add Emp) ∧ Bet_Point (Se p p2) p1 ∧ Line_on l1 p ∧ ¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p) add Emp)"

locale Order_Rule = Axiom_2 +
  assumes Bet_Point_Eq : "⟦Bet_Point (Se p1 p2) p3; Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)⟧ ⟹ Bet_Point (Se p4 p2) p3"
    and Line_on_Seg_rule : "Line_on_Seg l1 (Se p1 p2) ⟷ (∃p. Line_on l1 p ∧ Bet_Point (Se p1 p2) p)"
    and Seg_on_Seg_rule : "Seg_on_Seg (Se p1 p2) (Se p3 p4) ⟷ (∃p. Bet_Point (Se p1 p2) p ∧ Bet_Point (Se p3 p4) p)"
    and Line_on_Line_rule : "Line_on_Line l1 l2 ⟷ (∃p. Line_on l1 p ∧ Line_on l2 p)"
    and Seg_Point_Eq : "⟦Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)⟧ ⟹ Eq (Geos (Seg (Se p3 p1)) add Emp) (Geos (Seg (Se p3 p2)) add Emp)"

lemma(in Order_Rule) Line_Bet_on : 
  assumes
    "Bet_Point (Se p1 p2) p3"
  shows "Line_on (Li p1 p2) p3" and "Line_on (Li p2 p1) p3"
    and "Line_on (Li p2 p3) p1" and "Line_on (Li p3 p2) p1"
    and "Line_on (Li p1 p3) p2" and "Line_on (Li p3 p1) p2"
proof -
  from assms have "∃l. Line_on l p1 ∧ Line_on l p2 ∧ Line_on l p3" by (blast intro:Line_Bet_exist)
  then obtain l1 :: Line where P1 : "Line_on l1 p1 ∧ Line_on l1 p2 ∧ Line_on l1 p3" by blast
  from assms have P2 : "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)" by (simp add:Bet_Point_def)
  have P3 : "Line_on (Li p1 p2) p1 ∧ Line_on (Li p1 p2) p2" by (simp add:Line_on_rule)
  from P1 have P4 : "Line_on l1 p1" by simp
  from P1 have P5 : "Line_on l1 p2" by simp
  from P2 P3 P4 P5 have P6 : "Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li p1 p2)) add Emp)" by (simp add:Line_unique)
  from P1 P6 show P7 : "Line_on (Li p1 p2) p3" by (simp add:Line_on_trans)
  from assms have P8 : "¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)" by (simp add:Bet_Point_def)
  from P2 P7 P8 show "Line_on (Li p1 p3) p2" by (blast intro:Line_on_rev Eq_rev)
  from P2 P7 P8 show "Line_on (Li p3 p1) p2" by (blast intro:Line_on_trans Line_on_rev Eq_rev Line_rev)
  from P2 P7 show "Line_on (Li p2 p1) p3" by (blast intro:Line_on_trans Line_rev)
  from assms have P9 : "¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)" by (simp add:Bet_Point_def)
  from P2 P7 P9 show "Line_on (Li p2 p3) p1" by (blast intro:Line_on_rev Line_on_trans Line_rev Eq_rev)
  from P9 have P10 : "¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p2) add Emp)" by (blast intro:Eq_rev)
  from assms P2 P7 P8 P10 show "Line_on (Li p3 p2) p1" by (blast intro:Line_on_rev Bet_Point_def Line_on_trans Eq_rev Line_rev)
qed

lemma(in Order_Rule) Line_Bet_not_Eq :
  assumes N :
    "Bet_Point (Se p1 p2) p3"
    "¬ Line_on (Li p1 p2) p4"
  shows "¬ Eq (Geos (Lin (Li p4 p3)) add Emp) (Geos (Lin (Li p4 p2)) add Emp)" 
proof 
  assume W : "Eq (Geos (Lin (Li p4 p3)) add Emp) (Geos (Lin (Li p4 p2)) add Emp)" 
  have P1 : "Line_on (Li p4 p3) p3" by (simp add:Line_on_rule)
  from W P1 have P2 : "Line_on (Li p4 p2) p3" by (simp add:Line_on_trans)
  have P3 : "Line_on (Li p4 p2) p2" by (simp add:Line_on_rule)
  from N have P4 : "Line_on (Li p1 p2) p3" by (simp add:Line_Bet_on)
  have P5 : "Line_on (Li p1 p2) p2" by (simp add:Line_on_rule)
  from assms have P6 : "¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p3) add Emp)" by (simp add:Bet_Point_def)
  from P2 P3 P4 P5 P6 have P7 : "Eq (Geos (Lin (Li p4 p2)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)" by (simp add:Line_unique)
  have P8 : "Line_on (Li p4 p2) p4" by (simp add:Line_on_rule)
  from P7 P8 have P9 : "Line_on (Li p1 p2) p4" by (simp add:Line_on_trans)
  from N P9 show False by simp
qed

text‹Theorem3›

theorem(in Order_Rule) Seg_density :
  assumes "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)"
  shows "∃p. Bet_Point (Se A C) p" 
proof -
  have "∃p q r. ¬ Line_on (Li A C) p ∧ ¬ Line_on (Li A C) q ∧ ¬ Line_on (Li A C) r
        ∧ ¬ Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) ∧ ¬ Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp)
        ∧ ¬ Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)" by (blast intro:Line_not_on_exist)
  then obtain E :: Point where P1 : "¬ Line_on (Li A C) E" by blast
  then have P2 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)" by (simp add:Line_not_on_Point)
  have P3 : "Line_on (Li A E) A ∧ Line_on (Li A E) E" by (simp add:Line_on_rule)
  from P2 P3 have "∃p. Bet_Point (Se A p) E ∧ Line_on (Li A E) p" by (simp add:Bet_extension)
  then obtain F :: Point where P4 : "Bet_Point (Se A F) E ∧ Line_on (Li A E) F" by blast
  then have P5 : "Line_on (Li A F) E" by (simp add:Line_Bet_on)
  from P4 have P6 : "Bet_Point (Se A F) E" by simp
  from P6 have P7 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi F) add Emp)" by (simp add:Bet_Point_def)
  from P2 P4 P6 P7 have P8 : "Line_on (Li A E) F" by (simp add:Line_on_rev)
  from assms P1 have P9 : "¬ Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li A E)) add Emp)" by (simp add:Line_not_Eq)
  have P10 : "Line_on (Li A F) A" by (simp add:Line_on_rule)
  from P2 P3 P5 P10 have P11 : "Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li A F)) add Emp)" by (blast intro:Line_unique)
  from P9 P11 have P12 : "¬ Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li A F)) add Emp)" by (simp add:Eq_not_trans)
  from assms P7 P12 have P13 : "¬ Line_on (Li A C) F" by (simp add:Line_not_Eq_on)
  from assms P7 P13 have P14 : "¬ Line_on (Li A F) C" by (blast intro:Line_on_rev)
  have "Line_on (Li A F) F" by (simp add:Line_on_rule)
  then have P15 : "Eq (Geos (Poi F) add Emp) (Geos (Poi C) add Emp) ⟹ Line_on (Li A F) C" by (simp add:Point_Eq)
  from P14 P15 have P16 : "¬ Eq (Geos (Poi F) add Emp) (Geos (Poi C) add Emp)" by blast
  have P17 : "Line_on (Li F C) F ∧ Line_on (Li F C) C" by (simp add:Line_on_rule)
  from P16 P17 have "∃p. Bet_Point (Se F p) C ∧ Line_on (Li F C) p" by (simp add:Bet_extension)
  then obtain G :: Point where P18 : "Bet_Point (Se F G) C ∧ Line_on (Li F C) G" by blast
  from P18 have P19 : "Line_on (Li F G) C" by (simp add:Line_Bet_on)
  from P18 have P20 : "Bet_Point (Se F G) C" by simp
  then have P21 : "¬ Eq (Geos (Poi F) add Emp) (Geos (Poi G) add Emp)" by (simp add:Bet_Point_def)
  from P20 have P22 : "Line_on (Li F C) G" by (simp add:Line_Bet_on)
  from P7 P14 P21 P22 have P23 : "¬ Line_on (Li A F) G" by (simp add:Line_cross_not_on)
  from P6 P23 have P24 : "¬ Eq (Geos (Lin (Li G E)) add Emp) (Geos (Lin (Li G F)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from P5 have P25 : "Eq (Geos (Poi E) add Emp) (Geos (Poi G) add Emp) ⟹ Line_on (Li A F) G" by (simp add:Point_Eq)
  from P23 P25 have P26 : "¬ Eq (Geos (Poi G) add Emp) (Geos (Poi E) add Emp)" by (blast intro:Eq_rev)
  from P21 have P27 : "¬ Eq (Geos (Poi G) add Emp) (Geos (Poi F) add Emp)" by (blast intro:Eq_rev)
  from P24 P26 P27 have P28 : "¬ Line_on (Li G E) F" by (simp add:Line_not_Eq_on)
  from P26 P28 have P29 : "¬ Line_on (Li E G) F" by (blast intro:Line_rev Line_on_trans Eq_rev)
  have P30 : "Line_on (Li E G) E" by (simp add:Line_on_rule)
  have P31 : "Line_on (Li A E) E" by (simp add:Line_on_rule)
  have P32 : "Line_on (Li A E) A" by (simp add:Line_on_rule)
  from P2 P30 P31 P32 have P33 : "Line_on (Li E G) A ⟹ Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li E G)) add Emp)" by (simp add:Line_unique)
  from P8 P33 have P34 : "Line_on (Li E G) A ⟹ Line_on (Li E G) F" by (simp add:Line_on_trans)
  from P29 P34 have P35 : "¬ Line_on (Li E G) A" by blast
  have P36 : "Line_on (Li E G) G" by (simp add:Line_on_rule)
  have P37 : "Line_on (Li F G) G" by (simp add:Line_on_rule)
  from P20 have P38 : "¬ Eq (Geos (Poi G) add Emp) (Geos (Poi C) add Emp)" by (simp add:Bet_Point_def)
  from P19 P36 P37 P38 have P39 : "Line_on (Li E G) C ⟹ Eq (Geos (Lin (Li F G)) add Emp) (Geos (Lin (Li E G)) add Emp)" by (simp add:Line_unique)
  have P40 : "Line_on (Li F G) F" by (simp add:Line_on_rule)
  from P39 P40 have P41 : "Line_on (Li E G) C ⟹ Line_on (Li E G) F" by (simp add:Line_on_trans)
  from P29 P41 have P42 : "¬ Line_on (Li E G) C" by blast
  from P6 P14 P29 P30 P35 P42 have P43 : "Line_on_Seg (Li E G) (Se A C) ∧ ¬ Line_on_Seg (Li E G) (Se F C) ∨ Line_on_Seg (Li E G) (Se F C) ∧ ¬ Line_on_Seg (Li E G) (Se A C)" by (simp add:Pachets_axiom)
  then have "Line_on_Seg (Li E G) (Se F C) ⟹ ∃p. Line_on (Li E G) p ∧ Bet_Point (Se F C) p" by (simp add:Line_on_Seg_rule)
  then obtain D :: Point where P44 : "Line_on_Seg (Li E G) (Se F C) ⟹ Line_on (Li E G) D ∧ Bet_Point (Se F C) D" by blast
  from P44 have P46 : "Line_on_Seg (Li E G) (Se F C) ⟹ Bet_Point (Se F C) D" by simp
  from P46 have "Line_on_Seg (Li E G) (Se F C) ⟹ ¬ Eq (Geos (Poi D) add Emp) (Geos (Poi F) add Emp)" by (simp add:Bet_Point_def)
  from P46 have P47 : "Line_on_Seg (Li E G) (Se F C) ⟹ Line_on (Li F D) C" by (simp add:Line_Bet_on)
  have P48 : "Line_on (Li F D) F" by (simp add:Line_on_rule)
  have P49 : "Line_on (Li F G) F" by (simp add:Line_on_rule)
  from P16 P19 P47 P48 P49 have P50 : "Line_on_Seg (Li E G) (Se F C) ⟹  
    Eq (Geos (Lin (Li F D)) add Emp) (Geos (Lin (Li F G)) add Emp)" by (simp add:Line_unique)
  have P51 : "Line_on (Li F D) D" by (simp add:Line_on_rule)
  from P50 P51 have P52 : "Line_on_Seg (Li E G) (Se F C) ⟹ Line_on (Li F G) D" by (simp add:Line_on_trans)
  have P53 : "Line_on (Li F G) G" by (simp add:Line_on_rule)
  have P54 : "Line_on (Li E G) G" by (simp add:Line_on_rule)
  from P46 have P55 : "Line_on_Seg (Li E G) (Se F C) ⟹ Eq (Geos (Poi D) add Emp) (Geos (Poi G) add Emp) 
    ⟹ Bet_Point (Se F C) G" by (simp add:Point_Eq)
  from P20 have "Inv (Bet_Point (Se G C) F) ∧ Inv (Bet_Point (Se C F) G)" by (simp add:Bet_iff)
  then have "¬ Bet_Point (Se C F) G" by (simp add:Inv_def)
  then have P56 : "¬ Bet_Point (Se F C) G" by (blast intro:Bet_rev)
  from P55 P56 have P57 : "Line_on_Seg (Li E G) (Se F C) ⟹ ¬ Eq (Geos (Poi D) add Emp) (Geos (Poi G) add Emp)" by blast
  from P44 P52 P53 P54 P57 have P58 : "Line_on_Seg (Li E G) (Se F C) ⟹ 
    Eq (Geos (Lin (Li E G)) add Emp) (Geos (Lin (Li F G)) add Emp)" by (blast intro:Line_unique)
  from P26 have P59 : "Eq (Geos (Lin (Li E G)) add Emp) (Geos (Lin (Li G E)) add Emp)" by (simp add:Line_rev Eq_rev)
  from P27 have P60 : "Eq (Geos (Lin (Li F G)) add Emp) (Geos (Lin (Li G F)) add Emp)" by (simp add:Line_rev Eq_rev)
  from P58 P59 P60 have P61 : "Line_on_Seg (Li E G) (Se F C) ⟹ 
    Eq (Geos (Lin (Li G E)) add Emp) (Geos (Lin (Li G F)) add Emp)" by (blast intro:Eq_trans Eq_rev)
  from P24 P61 have P62 : "¬ Line_on_Seg (Li E G) (Se F C)" by blast
  from P43 P62 have "Line_on_Seg (Li E G) (Se A C) ∧ ¬ Line_on_Seg (Li E G) (Se F C)" by blast
  then have "∃p. Line_on (Li E G) p ∧ Bet_Point (Se A C) p" by (simp add:Line_on_Seg_rule)
  thus "∃p. Bet_Point (Se A C) p" by blast
qed

lemma(in Order_Rule) Line_Bet_not_on : 
  assumes 
    "Line_on (Li p1 p2) p3"
    "¬ Line_on (Li p1 p2) p4"
    "Bet_Point (Se p3 p4) p5"
  shows "Inv (Line_on (Li p1 p2) p5)" 
proof -
  from assms have "¬ Eq (Geos (Poi p5) add Emp) (Geos (Poi p3) add Emp)" by (simp add:Bet_Point_def)
  then have P1 : "¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)" by (blast intro:Eq_rev)
  from assms have P2 : "Line_on (Li p3 p5) p4" by (simp add:Line_Bet_on)
  have P3 : "Line_on (Li p3 p5) p3" by (simp add:Line_on_rule)
  have P4 : "Line_on (Li p3 p5) p5" by (simp add:Line_on_rule)
  from assms P1 P3 P4 have P5 : "Line_on (Li p1 p2) p5 ⟹ Eq (Geos (Lin (Li p3 p5)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)" by (simp add:Line_unique)
  from P2 P5 have P6 : "Line_on (Li p1 p2) p5 ⟹ Line_on (Li p1 p2) p4" by (simp add:Line_on_trans)
  from assms P6 have "¬ Line_on (Li p1 p2) p5" by blast
  thus "Inv (Line_on (Li p1 p2) p5)" by (simp add:Inv_def)
qed

lemma(in Order_Rule) Line_not_on_ex : 
  assumes N :
    "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)"
    "¬ Line_on (Li p1 p2) p3"
    "Line_on (Li p1 p4) p2"
  shows "¬ Line_on (Li p1 p4) p3" 
proof 
  assume W : "Line_on (Li p1 p4) p3" 
  have P1 : "Line_on (Li p1 p2) p2" by (simp add:Line_on_rule)
  have P2 : "Line_on (Li p1 p2) p1" by (simp add:Line_on_rule)
  have P3 : "Line_on (Li p1 p4) p1" by (simp add:Line_on_rule)
  from N P1 P2 P3 have P4 : "Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin (Li p1 p2)) add Emp)" by (simp add:Line_unique)
  from W P4 have P5 : "Line_on (Li p1 p2) p3" by (simp add:Line_on_trans)
  from N P5 show False by simp
qed

lemma(in Order_Rule) Line_on_dens : 
  assumes
    "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)"
    "¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p4) add Emp)"
    "Line_on (Li p1 p2) p3"
    "Line_on (Li p1 p4) p3"
  shows "Line_on (Li p2 p4) p3" 
proof -
  have P1 : "Line_on (Li p1 p2) p1" by (simp add:Line_on_rule)
  have P2 : "Line_on (Li p1 p4) p1" by (simp add:Line_on_rule)
  from assms P1 P2 have P3 : "Eq (Geos (Lin (Li p1 p2)) add Emp) (Geos (Lin (Li p1 p4)) add Emp)" by (simp add:Line_unique)
  have P4 : "Line_on (Li p1 p2) p2" by (simp add:Line_on_rule)
  from P3 P4 have P5 : "Line_on (Li p1 p4) p2" by (simp add:Line_on_trans)
  have P6 : "Line_on (Li p1 p4) p4" by (simp add:Line_on_rule)
  have P7 : "Line_on (Li p2 p4) p2" by (simp add:Line_on_rule)
  have P8 : "Line_on (Li p2 p4) p4" by (simp add:Line_on_rule)
  from assms P5 P6 P7 P8 have P9 : "Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin (Li p2 p4)) add Emp)" by (simp add:Line_unique)
  from assms P9 show "Line_on (Li p2 p4) p3" by (simp add:Line_on_trans)
qed

lemma(in Order_Rule) Bet_case_lemma1 : 
  assumes 
    "Line_on l1 A"
    "Line_on l1 B"
    "Line_on l1 C"
    "¬ Bet_Point (Se B A) C"
    "¬ Bet_Point (Se C B) A"
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
    "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
    "¬ Line_on (Li A C) D"
    "Bet_Point (Se B G) D"
  shows "∃p. Line_on (Li A D) p ∧ Bet_Point (Se G C) p"
proof -
  have P1 : "Line_on (Li A C) A" by (simp add:Line_on_rule)
  have P2 : "Line_on (Li A C) C" by (simp add:Line_on_rule)
  from assms P1 P2 have P3 : "Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from assms P3 have P4 : "Line_on (Li A C) B" by (simp add:Line_on_trans)
  have P11 : "Line_on (Li B G) B" by (simp add:Line_on_rule)
  from assms P2 P4 P11 have P12 : "Line_on (Li B G) C ⟹ Eq (Geos (Lin (Li B G)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from assms have P13 : "Line_on (Li B G) D" by (simp add:Line_Bet_on)
  from P12 P13 have P14 : "Line_on (Li B G) C ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from assms P14 have P15 : "¬ Line_on (Li B G) C" by blast
  have P16 : "Line_on (Li A D) A" by (simp add:Line_on_rule)
  from assms P1 P4 P16 have P17 : "Line_on (Li A D) B ⟹ Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  have P18 : "Line_on (Li A D) D" by (simp add:Line_on_rule)
  from P17 P18 have P19 : "Line_on (Li A D) B ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from assms P19 have P20 : "¬ Line_on (Li A D) B" by blast
  from assms P1 P2 P16 have P21 : "Line_on (Li A D) C ⟹ Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P18 P21 have P22 : "Line_on (Li A D) C ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from assms P22 have P23 : "¬ Line_on (Li A D) C" by blast
  from assms P1 P4 P11 have P24 : "Line_on (Li B G) A ⟹ Eq (Geos (Lin (Li B G)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P13 P24 have P25 : "Line_on (Li B G) A ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from assms P25 have P26 : "¬ Line_on (Li B G) A" by blast
  have P27 : "Line_on (Li B G) G" by (simp add:Line_on_rule)
  from assms have P28 : "¬ Eq (Geos (Poi G) add Emp) (Geos (Poi D) add Emp)" by (simp add:Bet_Point_def)
  from P13 P18 P27 P28 have P29 : "Line_on (Li A D) G ⟹ Eq (Geos (Lin (Li A D)) add Emp) (Geos (Lin (Li B G)) add Emp)" by (simp add:Line_unique)
  from P16 P29 have P30 : "Line_on (Li A D) G ⟹ Line_on (Li B G) A" by (simp add:Line_on_trans)
  from P26 P30 have P31 : "¬ Line_on (Li A D) G" by blast
  from assms P15 P18 P20 P23 P31 have P32 : "Line_on_Seg (Li A D) (Se B C) ∧ ¬ Line_on_Seg (Li A D) (Se G C)
    ∨ Line_on_Seg (Li A D) (Se G C) ∧ ¬ Line_on_Seg (Li A D) (Se B C)" by (simp add:Pachets_axiom)
  have "Line_on_Seg (Li A D) (Se B C) ⟹ ∃p. Line_on (Li A D) p ∧ Bet_Point (Se B C) p" by (simp add:Line_on_Seg_rule)
  then obtain A2 :: Point where P33 : "Line_on_Seg (Li A D) (Se B C) ⟹ Line_on (Li A D) A2 ∧ Bet_Point (Se B C) A2" by blast
  from assms have P34 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)" by (blast intro:Eq_rev)
  from assms P34 have P35 : "¬ Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li A D)) add Emp)" by (simp add:Line_not_Eq)
  have P36 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  have P37 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  from assms P2 P4 P36 P37 have P38 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P33 have P39 : "Line_on_Seg (Li A D) (Se B C) ⟹ Bet_Point (Se B C) A2" by simp
  then have P40 : "Line_on_Seg (Li A D) (Se B C) ⟹ Line_on (Li B C) A2" by (simp add:Line_Bet_on)
  from P38 P40 have P41 : "Line_on_Seg (Li A D) (Se B C) ⟹ Line_on (Li A C) A2" by (simp add:Line_on_trans)
  from P1 P16 P33 P35 P41 have P42 : "Line_on_Seg (Li A D) (Se B C) ⟹ Eq (Geos (Poi A2) add Emp) (Geos (Poi A) add Emp)" by (simp add:Line_unique_Point)
  from P39 P42 have P43 : "Line_on_Seg (Li A D) (Se B C) ⟹ Bet_Point (Se B C) A" by (simp add:Point_Eq)
  from assms have P44 : "¬ Bet_Point (Se B C) A" by (blast intro:Bet_rev)
  from P43 P44 have P45 : "¬ Line_on_Seg (Li A D) (Se B C)" by blast
  from P32 P45 have "Line_on_Seg (Li A D) (Se G C) ∧ ¬ Line_on_Seg (Li A D) (Se B C)" by blast
  thus "∃p. Line_on (Li A D) p ∧ Bet_Point (Se G C) p" by (simp add:Line_on_Seg_rule)
qed

lemma(in Order_Rule) Bet_case_lemma2 : 
  assumes 
    "Line_on l1 A"
    "Line_on l1 B"
    "Line_on l1 C"
    "¬ Bet_Point (Se B A) C"
    "¬ Bet_Point (Se C B) A"
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
    "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
  shows "Bet_Point (Se A C) B"
proof -
  have P1 : "Line_on (Li A C) A" by (simp add:Line_on_rule)
  have P2 : "Line_on (Li A C) C" by (simp add:Line_on_rule)
  from assms P1 P2 have P3 : "Eq (Geos (Lin l1) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from assms P3 have P4 : "Line_on (Li A C) B" by (simp add:Line_on_trans)
  have "∃p q r. ¬ Line_on (Li A C) p ∧ ¬ Line_on (Li A C) q ∧ ¬ Line_on (Li A C) r
    ∧ ¬ Eq (Geos (Poi p) add Emp) (Geos (Poi q) add Emp) ∧ ¬ Eq (Geos (Poi q) add Emp) (Geos (Poi r) add Emp)
    ∧ ¬ Eq (Geos (Poi r) add Emp) (Geos (Poi p) add Emp)" by (blast intro:Line_not_on_exist)
  then obtain D :: Point where P5 : "¬ Line_on (Li A C) D" by blast
  from P4 have P6 : "Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp) ⟹ Line_on (Li A C) D" by (simp add:Point_Eq)
  from P5 P6 have P7 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)" by blast
  have P8 : "Line_on (Li B D) B" by (simp add:Line_on_rule)
  have P9 : "Line_on (Li B D) D" by (simp add:Line_on_rule)
  from P7 P8 P9 have "∃p. Bet_Point (Se B p) D ∧ Line_on (Li B D) p" by (simp add:Bet_extension)
  then obtain G :: Point where P10 : "Bet_Point (Se B G) D" by blast
  from assms P5 P10 have "∃p. Line_on (Li A D) p ∧ Bet_Point (Se G C) p" by (simp add:Bet_case_lemma1)
  then obtain E :: Point where P11 : "Line_on (Li A D) E ∧ Bet_Point (Se G C) E" by blast
  from assms have P12 : "¬ Bet_Point (Se B C) A" by (blast intro:Bet_rev)
  from assms have P13 : "¬ Bet_Point (Se A B) C" by (blast intro:Bet_rev)
  from assms have P14 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi C) add Emp)" by (blast intro:Eq_rev)
  from assms have P15 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)" by (blast intro:Eq_rev)
  from assms have P16 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)" by (blast intro:Eq_rev)
  from P14 have P17 : "Eq (Geos (Lin (Li A C)) add Emp) (Geos (Lin (Li C A)) add Emp)" by (simp add:Line_rev)
  from P5 P17 have P18 : "¬ Line_on (Li C A) D" by (simp add:Line_not_on_trans)
  from assms P10 P12 P13 P14 P15 P16 P18 have "∃p. Line_on (Li C D) p ∧ Bet_Point (Se G A) p" by (simp add:Bet_case_lemma1)
  then obtain F :: Point where P19 : "Line_on (Li C D) F ∧ Bet_Point (Se G A) F" by blast
  have P20 : "Line_on (Li B G) B" by (simp add:Line_on_rule)
  have P21 : "Line_on (Li B G) G" by (simp add:Line_on_rule)
  from P10 have P22 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi G) add Emp)" by (simp add:Bet_Point_def)
  from P4 P20 P21 P22 have P23 : "Line_on (Li A C) G ⟹ Eq (Geos (Lin (Li B G)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P10 have P24 : "Line_on (Li B G) D" by (simp add:Line_Bet_on)
  from P23 P24 have P25 : "Line_on (Li A C) G ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from P5 P25 have P26 : "¬ Line_on (Li A C) G" by blast
  from P11 have P27 : "Bet_Point (Se C G) E" by (blast intro:Bet_rev)
  have P28 : "Line_on (Li C G) C" by (simp add:Line_on_rule)
  from assms P1 P2 P28 have P29 : "Line_on (Li C G) A ⟹ Eq (Geos (Lin (Li C G)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  have P30 : "Line_on (Li C G) G" by (simp add:Line_on_rule)
  from P29 P30 have P31 : "Line_on (Li C G) A ⟹ Line_on (Li A C) G" by (simp add:Line_on_trans)
  from P26 P31 have P32 : "¬ Line_on (Li C G) A" by blast
  from P27 P32 have "¬ Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li A G)) add Emp)" by (simp add:Line_Bet_not_Eq)
  then have P33 : "¬ Eq (Geos (Lin (Li A G)) add Emp) (Geos (Lin (Li A E)) add Emp)" by (blast intro:Eq_rev)
  from P19 have P34 : "Bet_Point (Se A G) F" by (blast intro:Bet_rev)
  then have P35 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi G) add Emp)" by (simp add:Bet_Point_def)
  from P27 have P36 : "Line_on (Li C G) E" by (simp add:Line_Bet_on)
  then have P37 : "Eq (Geos (Poi E) add Emp) (Geos (Poi A) add Emp) ⟹ Line_on (Li C G) A" by (simp add:Point_Eq)
  from P32 P37 have P38 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)" by (blast intro:Eq_rev)
  from P33 P35 P38 have P39 : "¬ Line_on (Li A G) E" by (simp add:Line_not_Eq_on)
  from P14 P26 P35 have P40 : "¬ Line_on (Li A G) C" by (blast intro:Line_on_rev)
  from P34 P40 have P41 : "¬ Eq (Geos (Lin (Li C F)) add Emp) (Geos (Lin (Li C G)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from P34 have P42 : "Line_on (Li A G) F" by (simp add:Line_Bet_on)
  then have P43 : "Eq (Geos (Poi F) add Emp) (Geos (Poi C) add Emp) ⟹ Line_on (Li A G) C" by (simp add:Point_Eq)
  from P40 P43 have P44 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi F) add Emp)" by (blast intro:Eq_rev)
  from P27 have P45 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi G) add Emp)" by (simp add:Bet_Point_def)
  from P41 P44 P45 have P46 : "¬ Line_on (Li C F) G" by (simp add:Line_not_Eq_on)
  from P35 have P47 : "Eq (Geos (Lin (Li A G)) add Emp) (Geos (Lin (Li G A)) add Emp)" by (simp add:Line_rev)
  from P40 P47 have P48 : "¬ Line_on (Li G A) C" by (simp add:Line_not_on_trans)
  from P19 have P49 : "Bet_Point (Se G A) F" by simp
  from P48 P49 have P50 : "¬ Eq (Geos (Lin (Li C F)) add Emp) (Geos (Lin (Li C A)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from assms P44 P50 have P51 : "¬ Line_on (Li C F) A" by (simp add:Line_not_Eq_on)
  have P52 : "Line_on (Li C F) C" by (simp add:Line_on_rule)
  from P27 have P53 : "¬ Eq (Geos (Poi E) add Emp) (Geos (Poi C) add Emp)" by (simp add:Bet_Point_def)
  from P28 P36 P52 P53 have P54 : "Line_on (Li C F) E ⟹ Eq (Geos (Lin (Li C G)) add Emp) (Geos (Lin (Li C F)) add Emp)" by (simp add:Line_unique)
  from P30 P54 have P55 : "Line_on (Li C F) E ⟹ Line_on (Li C F) G" by (simp add:Line_on_trans)
  from P46 P55 have P56 : "¬ Line_on (Li C F) E" by blast
  have P57 : "Line_on (Li C F) F" by (simp add:Line_on_rule)
  from P34 P39 P46 P51 P56 P57 have P58 : "Line_on_Seg (Li C F) (Se A E) ∧ ¬ Line_on_Seg (Li C F) (Se G E)
    ∨ Line_on_Seg (Li C F) (Se G E) ∧ ¬ Line_on_Seg (Li C F) (Se A E)" by (simp add:Pachets_axiom)
  have "Line_on_Seg (Li C F) (Se G E) ⟹ ∃p. Line_on (Li C F) p ∧ Bet_Point (Se G E) p" by (simp add:Line_on_Seg_rule)
  then obtain D2 :: Point where P59 : "Line_on_Seg (Li C F) (Se G E) ⟹ Line_on (Li C F) D2 ∧ Bet_Point (Se G E) D2" by blast
  then have P60 : "Line_on_Seg (Li C F) (Se G E) ⟹ Bet_Point (Se G E) D2" by simp
  then have P61 : "Line_on_Seg (Li C F) (Se G E) ⟹ Line_on (Li G E) D2" by (simp add:Line_Bet_on)
  have P62 : "Line_on (Li G E) G" by (simp add:Line_on_rule)
  have P63 : "Line_on (Li G E) E" by (simp add:Line_on_rule)
  from P27 have P64 : "¬ Eq (Geos (Poi G) add Emp) (Geos (Poi E) add Emp)" by (simp add:Bet_Point_def)
  from P27 have P66 : "Line_on (Li G E) C" by (simp add:Line_Bet_on)
  from P59 have P67 : "Line_on_Seg (Li C F) (Se G E) ⟹ Line_on (Li C F) D2" by simp
  from P60 have P68 : "Line_on_Seg (Li C F) (Se G E) ⟹ Eq (Geos (Poi D2) add Emp) (Geos (Poi C) add Emp) ⟹ 
    Bet_Point (Se G E) C" by (simp add:Point_Eq)
  from P27 have "Inv (Bet_Point (Se G E) C) ∧ Inv (Bet_Point (Se E C) G)" by (simp add:Bet_iff)
  then have P69 : "¬ Bet_Point (Se G E) C ∧ ¬ Bet_Point (Se E C) G" by (simp add:Inv_def)
  from P68 P69 have P70 : "Line_on_Seg (Li C F) (Se G E) ⟹ ¬ Eq (Geos (Poi D2) add Emp) (Geos (Poi C) add Emp)" by blast
  from P52 P61 P66 P67 P70 have P71 : "Line_on_Seg (Li C F) (Se G E) ⟹ Eq (Geos (Lin (Li G E)) add Emp) (Geos (Lin (Li C F)) add Emp)" by (simp add:Line_unique)
  from P63 P71 have P72 : "Line_on_Seg (Li C F) (Se G E) ⟹ Line_on (Li C F) E" by (simp add:Line_on_trans)
  from P56 P72 have P73 : "¬ Line_on_Seg (Li C F) (Se G E)" by blast
  from P58 P73 have "Line_on_Seg (Li C F) (Se A E) ∧ ¬ Line_on_Seg (Li C F) (Se G E)" by blast
  then have "∃p. Line_on (Li C F) p ∧ Bet_Point (Se A E) p" by (simp add:Line_on_Seg_rule)
  then obtain D3 :: Point where P74 : "Line_on (Li C F) D3 ∧ Bet_Point (Se A E) D3" by blast
  then have P75 : "Line_on (Li C F) D3" by simp
  from P74 have P76 : "Bet_Point (Se A E) D3" by simp
  then have P77 : "Line_on (Li A E) D3" by (simp add:Line_Bet_on)
  from P19 have P78 : "Line_on (Li C D) F" by simp
  from P2 have P79 : "Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp) ⟹ Line_on (Li A C) D" by (simp add:Point_Eq)
  from P5 P79 have P80 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi D) add Emp)" by blast
  from P44 P78 P80 have P81 : "Line_on (Li C F) D" by (simp add:Line_on_rev)
  from P11 have P82 : "Line_on (Li A D) E" by simp
  from P1 have P83 : "Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp) ⟹ Line_on (Li A C) D" by (simp add:Point_Eq)
  from P5 P83 have P84 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)" by blast
  from P38 P82 P84 have P85 : "Line_on (Li A E) D" by (simp add:Line_on_rev)
  have P86 : "Line_on (Li A E) E" by (simp add:Line_on_rule)
  then have P87 : "Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li C F)) add Emp) ⟹ Line_on (Li C F) E" by (simp add:Line_on_trans)
  from P56 P87 have P88 : "¬ Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li C F)) add Emp)" by blast
  from P75 P77 P81 P85 P88 have P89 : "Eq (Geos (Poi D3) add Emp) (Geos (Poi D) add Emp)" by (simp add:Line_unique_Point)
  from P76 P89 have P90 : "Bet_Point (Se A E) D" by (simp add:Point_Eq)
  have P91 : "Line_on (Li A E) A" by (simp add:Line_on_rule)
  from assms P1 P2 P91 have P92 : "Line_on (Li A E) C ⟹ Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P85 P92 have P93 : "Line_on (Li A E) C ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from P5 P93 have P94 : "¬ Line_on (Li A E) C" by blast
  from assms P1 P4 P20 have P95 : "Line_on (Li B G) A ⟹ Eq (Geos (Lin (Li B G)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P24 P95 have P96 : "Line_on (Li B G) A ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from P5 P96 have P97 : "¬ Line_on (Li B G) A" by blast
  from assms P2 P4 P20 have P98 : "Line_on (Li B G) C ⟹ Eq (Geos (Lin (Li B G)) add Emp) (Geos (Lin (Li A C)) add Emp)" by (simp add:Line_unique)
  from P24 P98 have P99 : "Line_on (Li B G) C ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from P5 P99 have P100 : "¬ Line_on (Li B G) C" by blast
  from P21 P62 P63 P64 have P101 : "Line_on (Li B G) E ⟹ Eq (Geos (Lin (Li G E)) add Emp) (Geos (Lin (Li B G)) add Emp)" by (simp add:Line_unique)
  from P66 P101 have P102 : "Line_on (Li B G) E ⟹ Line_on (Li B G) C" by (simp add:Line_on_trans)
  from P100 P102 have P103 : "¬ Line_on (Li B G) E" by blast
  from P24 P90 P94 P97 P100 P103 have P104 : "Line_on_Seg (Li B G) (Se A C) ∧ ¬ Line_on_Seg (Li B G) (Se E C)
    ∨ Line_on_Seg (Li B G) (Se E C) ∧ ¬ Line_on_Seg (Li B G) (Se A C)" by (simp add:Pachets_axiom)
  have "Line_on_Seg (Li B G) (Se E C) ⟹ ∃p. Line_on (Li B G) p ∧ Bet_Point (Se E C) p" by (simp add:Line_on_Seg_rule)
  then obtain B2 :: Point where P105 : "Line_on_Seg (Li B G) (Se E C) ⟹ Line_on (Li B G) B2 ∧ Bet_Point (Se E C) B2" by blast
  then have P106 : "Line_on_Seg (Li B G) (Se E C) ⟹ Bet_Point (Se E C) B2" by simp
  then have P107 : "Line_on_Seg (Li B G) (Se E C) ⟹ Line_on (Li E C) B2" by (simp add:Line_Bet_on)
  from P105 have P108 : "Line_on_Seg (Li B G) (Se E C) ⟹ Line_on (Li B G) B2" by simp
  have P109 : "Line_on (Li E C) E" by (simp add:Line_on_rule)
  have P110 : "Line_on (Li E C) C" by (simp add:Line_on_rule)
  from P28 P36 P53 P109 P110 have P111 : "Eq (Geos (Lin (Li C G)) add Emp) (Geos (Lin (Li E C)) add Emp)" by (simp add:Line_unique)
  from P30 P111 have P112 : "Line_on (Li E C) G" by (simp add:Line_on_trans)
  from P106 have P113 : "Line_on_Seg (Li B G) (Se E C) ⟹ Eq (Geos (Poi B2) add Emp) (Geos (Poi G) add Emp) ⟹
    Bet_Point (Se E C) G" by (simp add:Point_Eq)
  from P69 P113 have P114 : "Line_on_Seg (Li B G) (Se E C) ⟹ ¬ Eq (Geos (Poi B2) add Emp) (Geos (Poi G) add Emp)" by blast
  from P21 P107 P108 P112 P114 have P115 : "Line_on_Seg (Li B G) (Se E C) ⟹ Eq (Geos (Lin (Li E C)) add Emp) (Geos (Lin (Li B G)) add Emp)" by (simp add:Line_unique)
  from P109 P115 have P116 : "Line_on_Seg (Li B G) (Se E C) ⟹ Line_on (Li B G) E" by (simp add:Line_on_trans)
  from P103 P116 have P117 : "¬ Line_on_Seg (Li B G) (Se E C)" by blast
  from P104 P117 have "Line_on_Seg (Li B G) (Se A C)" by blast
  then have "∃p. Line_on (Li B G) p ∧ Bet_Point (Se A C) p" by (simp add:Line_on_Seg_rule)
  then obtain B3 :: Point where P118 : "Line_on (Li B G) B3 ∧ Bet_Point (Se A C) B3" by blast
  from P24 have P119 : "Eq (Geos (Lin (Li B G)) add Emp) (Geos (Lin (Li A C)) add Emp) ⟹ Line_on (Li A C) D" by (simp add:Line_on_trans)
  from P5 P119 have P120 : "¬ Eq (Geos (Lin (Li B G)) add Emp) (Geos (Lin (Li A C)) add Emp)" by blast
  from P118 have P121 : "Line_on (Li B G) B3" by simp
  from P118 have P122 : "Bet_Point (Se A C) B3" by simp
  then have P123 : "Line_on (Li A C) B3" by (simp add:Line_Bet_on)
  from P4 P20 P120 P121 P123 have P124 : "Eq (Geos (Poi B3) add Emp) (Geos (Poi B) add Emp)" by (simp add:Line_unique_Point)
  from P122 P124 show "Bet_Point (Se A C) B" by (simp add:Point_Eq)
qed

text‹Theorem4›

lemma(in Order_Rule) Bet_case : 
  assumes 
    "Line_on l1 A"
    "Line_on l1 B"
    "Line_on l1 C"
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)"
    "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi C) add Emp)"
    "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi A) add Emp)"
  shows "Bet_Point (Se A C) B ∨ Bet_Point (Se C B) A ∨ Bet_Point (Se B A) C"
proof -
  from assms have P1 : "¬ Bet_Point (Se B A) C ∧ ¬ Bet_Point (Se C B) A ⟹ Bet_Point (Se A C) B" by (simp add:Bet_case_lemma2)
  from assms have P2 : "¬ Bet_Point (Se C B) A ∧ ¬ Bet_Point (Se A C) B ⟹ Bet_Point (Se B A) C" by (simp add:Bet_case_lemma2)
  from assms have P3 : "¬ Bet_Point (Se A C) B ∧ ¬ Bet_Point (Se B A) C ⟹ Bet_Point (Se C B) A" by (simp add:Bet_case_lemma2)
  from P1 P2 P3 show "Bet_Point (Se A C) B ∨ Bet_Point (Se C B) A ∨ Bet_Point (Se B A) C" by blast
qed

lemma(in Order_Rule) Bet_case_fact : 
  assumes 
    "Bet_Point (Se A C) B ∨ Bet_Point (Se C B) A ∨ Bet_Point (Se B A) C"
  shows 
    "Bet_Point (Se A C) B ∧ ¬ Bet_Point (Se C B) A ∧ ¬ Bet_Point (Se B A) C
    ∨ ¬ Bet_Point (Se A C) B ∧ Bet_Point (Se C B) A ∧ ¬ Bet_Point (Se B A) C
    ∨ ¬ Bet_Point (Se A C) B ∧ ¬ Bet_Point (Se C B) A ∧ Bet_Point (Se B A) C"
proof -
  have "Bet_Point (Se A C) B ⟹ Inv (Bet_Point (Se C B) A) ∧ Inv (Bet_Point (Se B A) C)" by (simp add:Bet_iff)
  then have P1 : "Bet_Point (Se A C) B ⟹ ¬ Bet_Point (Se C B) A ∧ ¬ Bet_Point (Se B A) C" by (simp add:Inv_def)
  have "Bet_Point (Se C B) A ⟹ Inv (Bet_Point (Se A C) B) ∧ Inv (Bet_Point (Se B A) C)" by (simp add:Bet_iff)
  then have P2 : "Bet_Point (Se C B) A ⟹ ¬ Bet_Point (Se A C) B ∧ ¬ Bet_Point (Se B A) C" by (simp add:Inv_def)
  have "Bet_Point (Se B A) C ⟹ Inv (Bet_Point (Se A C) B) ∧ Inv (Bet_Point (Se C B) A)" by (simp add:Bet_iff)
  then have P3 : "Bet_Point (Se B A) C ⟹ ¬ Bet_Point (Se A C) B ∧ ¬ Bet_Point (Se C B) A" by (simp add:Inv_def)
  from assms P1 P2 P3 show "Bet_Point (Se A C) B ∧ ¬ Bet_Point (Se C B) A ∧ ¬ Bet_Point (Se B A) C
    ∨ ¬ Bet_Point (Se A C) B ∧ Bet_Point (Se C B) A ∧ ¬ Bet_Point (Se B A) C
    ∨ ¬ Bet_Point (Se A C) B ∧ ¬ Bet_Point (Se C B) A ∧ Bet_Point (Se B A) C" by blast
qed

lemma(in Order_Rule) Bet_swap_lemma_1 : 
  assumes
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)"
    "Bet_Point (Se A C) B"
    "Bet_Point (Se B D) C"
  shows "Line_on (Li A D) B ∧ Line_on (Li A D) C"
proof -
  from assms have P1 : "Line_on (Li A B) C" by (simp add:Line_Bet_on)
  have P2 : "Line_on (Li A B) B" by (simp add:Line_on_rule)
  have P3 : "Line_on (Li B C) C" by (simp add:Line_on_rule)
  have P4 : "Line_on (Li B C) B" by (simp add:Line_on_rule)
  from assms have P5 : "¬ Eq (Geos (Poi C) add Emp) (Geos (Poi B) add Emp)" by (simp add:Bet_Point_def)
  from P1 P2 P3 P4 P5 have P6 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A B)) add Emp)" by (simp add:Line_unique)
  from assms have P7 : "Line_on (Li B C) D" by (simp add:Line_Bet_on)
  from P6 P7 have P8 : "Line_on (Li A B) D" by (simp add:Line_on_trans)
  from assms have "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi A) add Emp)" by (simp add:Bet_Point_def)
  then have P9 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi B) add Emp)" by (blast intro:Eq_rev)
  from assms P8 P9 have P10 : "Line_on (Li A D) B" by (simp add:Line_on_rev)
  have P11 : "Line_on (Li A D) D" by (simp add:Line_on_rule)
  from assms have P12 : "¬ Eq (Geos (Poi B) add Emp) (Geos (Poi D) add Emp)" by (simp add:Bet_Point_def)
  from P4 P7 P10 P11 P12 have P13 : "Eq (Geos (Lin (Li B C)) add Emp) (Geos (Lin (Li A D)) add Emp)" by (simp add:Line_unique)
  from P3 P13 have P14 : "Line_on (Li A D) C" by (simp add:Line_on_trans)
  from P10 P14 show "Line_on (Li A D) B ∧ Line_on (Li A D) C" by simp
qed

lemma(in Order_Rule) Bet_swap_lemma_2 : 
  assumes
    "Bet_Point (Se p1 p3) p2"
    "¬ Line_on (Li p1 p3) p4"
    "¬ Line_on (Li p2 p5) p3"
    "¬ Line_on (Li p2 p5) p1"
    "¬ Line_on (Li p2 p5) p4"
    "Bet_Point (Se p3 p5) p4"
  shows "∃p. Line_on (Li p2 p5) p ∧ Bet_Point (Se p1 p4) p" 
proof -
  have P1 : "Line_on (Li p2 p5) p2" by (simp add:Line_on_rule)
  from assms P1 have P2 : "Line_on_Seg (Li p2 p5) (Se p1 p4) ∧ ¬ Line_on_Seg (Li p2 p5) (Se p3 p4) ∨ Line_on_Seg (Li p2 p5) (Se p3 p4) ∧ ¬ Line_on_Seg (Li p2 p5) (Se p1 p4)" by (simp add:Pachets_axiom)
  then have "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ ∃p. Line_on (Li p2 p5) p ∧ Bet_Point (Se p3 p4) p" by (simp add:Line_on_Seg_rule)
  then obtain p6 :: Point where P3 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ Line_on (Li p2 p5) p6 ∧ Bet_Point (Se p3 p4) p6" by blast
  from assms have "¬ Eq (Geos (Poi p4) add Emp) (Geos (Poi p3) add Emp)" by (simp add:Bet_Point_def)
  then have P4 : "¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p4) add Emp)" by (blast intro:Eq_rev)
  from P3 have P5 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ Bet_Point (Se p3 p4) p6" by simp
  from P3 have P6 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ Line_on (Li p3 p6) p4" by (simp add:Line_Bet_on)
  from assms have P7 : "Line_on (Li p3 p5) p4" by (simp add:Line_Bet_on)    
  have P8 : "Line_on (Li p3 p6) p3" by (simp add:Line_on_rule)
  have P9 : "Line_on (Li p3 p5) p3" by (simp add:Line_on_rule)
  from P4 P6 P7 P8 P9 have P10 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ 
    Eq (Geos (Lin (Li p3 p5)) add Emp) (Geos (Lin (Li p3 p6)) add Emp)" by (simp add:Line_unique)
  have P11 : "Line_on (Li p3 p5) p5" by (simp add:Line_on_rule)
  from P10 P11 have P12 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ Line_on (Li p3 p6) p5" by (simp add:Line_on_trans)
  have P13 : "Line_on (Li p2 p5) p5" by (simp add:Line_on_rule)
  have P14 : "Line_on (Li p3 p6) p6" by (simp add:Line_on_rule)
  from P5 have P15 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ Eq (Geos (Poi p6) add Emp) (Geos (Poi p5) add Emp) ⟹
    Bet_Point (Se p3 p4) p5" by (simp add:Point_Eq)
  from assms have "Inv (Bet_Point (Se p5 p4) p3) ∧ Inv (Bet_Point (Se p4 p3) p5)" by (simp add:Bet_iff)
  then have "¬ Bet_Point (Se p4 p3) p5" by (simp add:Inv_def)
  then have P16 : "¬ Bet_Point (Se p3 p4) p5" by (blast intro:Bet_rev)
  from P15 P16 have P17 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ ¬ Eq (Geos (Poi p6) add Emp) (Geos (Poi p5) add Emp)" by blast
  from P3 P12 P13 P14 P17 have P18 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ 
    Eq (Geos (Lin (Li p3 p6)) add Emp) (Geos (Lin (Li p2 p5)) add Emp)" by (simp add:Line_unique)
  from P8 P18 have P19 : "Line_on_Seg (Li p2 p5) (Se p3 p4) ⟹ Line_on (Li p2 p5) p3" by (simp add:Line_on_trans)
  from assms P19 have P20 : "¬ Line_on_Seg (Li p2 p5) (Se p3 p4)" by blast
  from P2 P3 P20 have "Line_on_Seg (Li p2 p5) (Se p1 p4)" by blast
  thus "∃p. Line_on (Li p2 p5) p ∧ Bet_Point (Se p1 p4) p" by (simp add:Line_on_Seg_rule)
qed

lemma(in Order_Rule) Bet_swap_lemma_3 : 
  assumes
    "Bet_Point (Se p1 p3) p2"
    "Bet_Point (Se p3 p5) p4"
    "¬ Line_on (Li p1 p3) p5"
  shows "∃p. Bet_Point (Se p1 p4) p ∧ Bet_Point (Se p5 p2) p" 
proof -
  from assms have P1 : "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p3) add Emp)" by (simp add:Bet_Point_def)
  then have P2 : "Eq (Geos (Lin (Li p1 p3)) add Emp) (Geos (Lin (Li p3 p1)) add Emp)" by (simp add:Line_rev)
  from assms P2 have P3 : "¬ Line_on (Li p3 p1) p5" by (simp add:Line_not_on_trans)
  from assms have P4 : "¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p5) add Emp)" by (simp add:Bet_Point_def)
  from P1 have P5 : "¬ Eq (Geos (Poi p3) add Emp) (Geos (Poi p1) add Emp)" by (blast intro:Eq_rev)
  from P3 P4 P5 have P6 : "¬ Line_on (Li p3 p5) p1" by (blast intro:Line_on_rev)
  from assms have P7 : "Bet_Point (Se p5 p3) p4" by (simp add:Bet_rev)
  from P4 have P8 : "Eq (Geos (Lin (Li p3 p5)) add Emp) (Geos (Lin (Li p5 p3)) add Emp)" by (simp add:Line_rev)
  from P8 P6 have P9 : "¬ Line_on (Li p5 p3) p1" by (simp add:Line_not_on_trans)
  from P7 P9 have P10 : "¬ Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin (Li p1 p3)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from assms have "Line_on (Li p3 p5) p4" by (simp add:Line_Bet_on)
  then have P11 : "Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp) ⟹ Line_on (Li p3 p5) p1" by (simp add:Point_Eq)
  from P6 P11 have "¬ Eq (Geos (Poi p4) add Emp) (Geos (Poi p1) add Emp)" by blast
  then have P12 : "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p4) add Emp)" by (blast intro:Eq_rev)
  from P1 P10 P12 have P13 : "¬ Line_on (Li p1 p4) p3" by (simp add:Line_not_Eq_on)
  from P1 P12 P13 have P14 : "¬ Line_on (Li p1 p3) p4" by (blast intro:Line_on_rev) 
  from assms have P15 : "¬ Eq (Geos (Lin (Li p5 p2)) add Emp) (Geos (Lin (Li p5 p3)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from assms have P16 : "Line_on (Li p1 p3) p2" by (simp add:Line_Bet_on)
  then have P17 : "Eq (Geos (Poi p2) add Emp) (Geos (Poi p5) add Emp) ⟹ Line_on (Li p1 p3) p5" by (simp add:Point_Eq)
  from assms P17 have "¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p5) add Emp)" by blast
  then have P18 : "¬ Eq (Geos (Poi p5) add Emp) (Geos (Poi p2) add Emp)" by (blast intro:Eq_rev)
  from P4 have P19 : "¬ Eq (Geos (Poi p5) add Emp) (Geos (Poi p3) add Emp)" by (blast intro:Eq_rev)
  from P15 P18 P19 have P20 : "¬ Line_on (Li p5 p2) p3" by (simp add:Line_not_Eq_on)
  from P18 have P21 : "Eq (Geos (Lin (Li p5 p2)) add Emp) (Geos (Lin (Li p2 p5)) add Emp)" by (simp add:Line_rev)
  from P20 P21 have P22 : "¬ Line_on (Li p2 p5) p3" by (simp add:Line_not_on_trans) 
  from assms have P23 :"Bet_Point (Se p3 p1) p2" by (blast intro:Bet_rev)
  from P3 P23 have P24 : "¬ Eq (Geos (Lin (Li p5 p2)) add Emp) (Geos (Lin (Li p5 p1)) add Emp)" by (simp add:Line_Bet_not_Eq)
  have "Line_on (Li p3 p1) p1" by (simp add:Line_on_rule)
  then have P25 : "Eq (Geos (Poi p1) add Emp) (Geos (Poi p5) add Emp) ⟹ Line_on (Li p3 p1) p5" by (simp add:Point_Eq)
  from P3 P25 have P26 : "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p5) add Emp)" by blast
  then have P27 : "¬ Eq (Geos (Poi p5) add Emp) (Geos (Poi p1) add Emp)" by (blast intro:Eq_rev)
  from P18 P24 P27 have P28 : "¬ Line_on (Li p5 p2) p1" by (simp add:Line_not_Eq_on)
  from P21 P28 have P29 : "¬ Line_on (Li p2 p5) p1" by (simp add:Line_not_on_trans) 
  from assms have P31 : "Line_on (Li p3 p4) p5" by (simp add:Line_Bet_on)
  have P32 : "Line_on (Li p3 p4) p4" by (simp add:Line_on_rule)
  have P33 : "Line_on (Li p2 p5) p5" by (simp add:Line_on_rule)
  from assms have P34 : "¬ Eq (Geos (Poi p5) add Emp) (Geos (Poi p4) add Emp)" by (simp add:Bet_Point_def)
  from P31 P32 P33 P34 have P35 : "Line_on (Li p2 p5) p4 ⟹ Eq (Geos (Lin (Li p3 p4)) add Emp) (Geos (Lin (Li p2 p5)) add Emp)" by (simp add:Line_unique)
  have P36 : "Line_on (Li p3 p4) p3" by (simp add:Line_on_rule)
  from P35 P36 have P37 : "Line_on (Li p2 p5) p4 ⟹ Line_on (Li p2 p5) p3" by (simp add:Line_on_trans)
  from P22 P37 have P38 : "¬ Line_on (Li p2 p5) p4" by blast
  from assms P14 P22 P29 P38 have "∃p. Line_on (Li p2 p5) p ∧ Bet_Point (Se p1 p4) p" by (simp add:Bet_swap_lemma_2)
  then obtain p6 :: Point where P39 : "Line_on (Li p2 p5) p6 ∧ Bet_Point (Se p1 p4) p6" by blast
  from P12 have P40 : "Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin (Li p4 p1)) add Emp)" by (simp add:Line_rev)
  from P13 P40 have P41 : "¬ Line_on (Li p4 p1) p3" by (simp add:Line_not_on_trans) 
  from assms P6 have P42 : "¬ Eq (Geos (Lin (Li p1 p4)) add Emp) (Geos (Lin (Li p1 p5)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from P12 P26 P42 have P43 : "¬ Line_on (Li p1 p4) p5" by (simp add:Line_not_Eq_on)
  from P40 P43 have P44 : "¬ Line_on (Li p4 p1) p5" by (simp add:Line_not_on_trans)
  from assms have "¬ Eq (Geos (Poi p2) add Emp) (Geos (Poi p1) add Emp)" by (simp add:Bet_Point_def)
  then have P45 : "¬ Eq (Geos (Poi p1) add Emp) (Geos (Poi p2) add Emp)" by (blast intro:Eq_rev)
  from P1 P16 P45 have P47 : "Line_on (Li p1 p2) p3" by (simp add:Line_on_rev)
  from P47 have P48 : "Eq (Geos (Lin (Li p1 p2)) add Emp) (Geos (Lin (Li p1 p4)) add Emp) ⟹ Line_on (Li p1 p4) p3" by (simp add:Line_on_trans)
  from P13 P48 have P49 : "¬ Eq (Geos (Lin (Li p1 p2)) add Emp) (Geos (Lin (Li p1 p4)) add Emp)" by blast
  from P12 P45 P49 have P50 : "¬ Line_on (Li p1 p2) p4" by (simp add:Line_not_Eq_on)
  from P12 P45 P50 have P51 : "¬ Line_on (Li p1 p4) p2" by (blast intro:Line_on_rev)
  from P40 P51 have P52 : "¬ Line_on (Li p4 p1) p2" by (simp add:Line_not_on_trans) 
  from P18 P19 P20 have P53 : "¬ Line_on (Li p5 p3) p2" by (blast intro:Line_on_rev)
  from P7 P23 P41 P44 P52 P53 have "∃p. Line_on (Li p4 p1) p ∧ Bet_Point (Se p5 p2) p" by (simp add:Bet_swap_lemma_2)
  then obtain p7 :: Point where P54 : "Line_on (Li p4 p1) p7 ∧ Bet_Point (Se p5 p2) p7" by blast
  from P33 P44 have P55 : "¬ Eq (Geos (Lin (Li p4 p1)) add Emp) (Geos (Lin (Li p2 p5)) add Emp)" by (simp add:Line_not_on_Eq)
  from P39 have P56 : "Line_on (Li p4 p1) p6" by (simp add:Line_Bet_on)
  from P54 have P57 : "Line_on (Li p2 p5) p7" by (simp add:Line_Bet_on)
  from P39 P54 P55 P56 P57 have P58 : "Eq (Geos (Poi p7) add Emp) (Geos (Poi p6) add Emp)" by (blast intro:Line_unique_Point)
  from P54 have P59 : "Bet_Point (Se p5 p2) p7" by simp
  from P58 P59 have P60 : "Bet_Point (Se p5 p2) p6" by (simp add:Point_Eq)
  from P39 P60 show "∃p. Bet_Point (Se p1 p4) p ∧ Bet_Point (Se p5 p2) p" by blast
qed

lemma(in Order_Rule) Bet_swap_lemma_4 : 
  assumes 
    "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi D) add Emp)"
    "Bet_Point (Se A E) G"
    "Bet_Point (Se D G) H"
    "¬ Line_on (Li A D) E"
  shows "∃p. Line_on (Li H E) p ∧ Bet_Point (Se D A) p"
proof -
  from assms have P1 : "¬ Eq (Geos (Poi A) add Emp) (Geos (Poi E) add Emp)" by (simp add:Bet_Point_def)
  from assms P1 have P2 : "¬ Line_on (Li A E) D" by (blast intro:Line_on_rev)
  from P1 have P3 : "Eq (Geos (Lin (Li A E)) add Emp) (Geos (Lin (Li E A)) add Emp)" by (simp add:Line_rev)
  from P2 P3 have P4 : "¬ Line_on (Li E A) D" by (simp add:Line_not_on_trans)
  from assms have P5 : "Bet_Point (Se E A) G" by (simp add:Bet_rev)
  from P4 P5 have P6 : "¬ Eq (Geos (Lin (Li D G)) add Emp) (Geos (Lin (Li D A)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from assms have P7 : "¬ Eq (Geos (Poi D) add Emp) (Geos (Poi G) add Emp)" by (simp add:Bet_Point_def)
  from assms have P8 : "¬ Eq (Geos (Poi D) add Emp) (Geos (Poi A) add Emp)" by (blast intro:Eq_rev)
  from P6 P7 P8 have P9 : "¬ Line_on (Li D G) A" by (simp add:Line_not_Eq_on)
  from assms P2 have P10 : "¬ Eq (Geos (Lin (Li D G)) add Emp) (Geos (Lin (Li D E)) add Emp)" by (simp add:Line_Bet_not_Eq)
  have "Line_on (Li A D) D" by (simp add:Line_on_rule)
  then have P11 : "Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp) ⟹ Line_on (Li A D) E" by (simp add:Point_Eq)
  from assms P11 have P12 : "¬ Eq (Geos (Poi D) add Emp) (Geos (Poi E) add Emp)" by blast
  from P7 P10 P12 have P13 : "¬ Line_on (Li D G) E" by (simp add:Line_not_Eq_on)
  from assms P13 have P14 : "¬ Eq (Geos (Lin (Li E H)) add Emp) (Geos (Lin (Li E G)) add Emp)" by (simp add:Line_Bet_not_Eq)
  from assms have "Line_on (Li D G) H" by (simp add:Line_Bet_on)
  then have P15 : "Eq (Geos (Poi H) add Emp) (Geos (Poi E) add Emp) ⟹ Line_on (Li D G) E" by (simp add:Point_Eq)
  from P13 P15 have P16 : "¬ Eq (Geos (Poi E) add Emp) (Geos (Poi H) add Emp)" by (blast intro:Eq_rev)
  from assms have "Line_on (Li D G) G" by (simp add:Line_on_rule)
  then have P17 : "Eq (Geos (Poi G) add Emp) (Geos (Poi E) add Emp) ⟹ Line_on (Li D G) E" by (simp add:Point_Eq)
  from P13 P17 have P18 : "¬ Eq (Geos (Poi E) add Emp) (Geos (Poi G) add Emp)" by (blast intro:Eq_rev)
  from P14 P16 P18 have P19 : "¬ Line_on (Li E H) G" by (simp add:Line_not_Eq_on)
  from P7 have P20 : "Eq (Geos (Lin (Li