(* Paste in these 4 commands, in two mouse copy/pastes    (setq case-fold-search nil)

   cd ~/hol_light; ocaml
   #use "hol.ml";; 

#load "unix.cma";;
loadt "miz3/miz3.ml";;

   and then paste in the following file. *)

(* ================================================================= *)
(* HOL Light Hilbert geometry axiomatic proofs. *)
(* ================================================================= *)

(* Thanks to Mizar folks who wrote an influential language I was able
   to learn, Freek Wiedijk, who wrote the miz3 port of Mizar to HOL
   Light, and especially John Harrison, who came up with the entire
   framework here of porting my axiomatic proofs to HOL Light.       *)


horizon := 0;; 

new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("===",`:point#point->point#point->bool`);;
new_constant("Line",`:point_set->bool`);;

parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("same_side",(12, "right"));;
parse_as_infix("int_angle",(12, "right"));;


let Interval_DEF = new_definition
  `!A B X. open_int (A,B) X <=> Between (A,X,B)`;;

let Collinear_DEF = new_definition
  `Collinear (A,B,C)  <=> 
  ?l. Line l /\  A IN l /\ B IN l /\ C IN l`;;

let same_side_DEF = new_definition
  `A,B same_side l <=> 
  Line l /\  ~(?X. (X IN l) /\  X IN open_int (A,B))`;;

let Ray_DEF = new_definition
  `!A B X. ray (A,B) X <=> ~(A = B) /\ Collinear (A,B,X) /\ ~(A IN open_int (X,B))`;;

let cong_DEF = new_definition
 `A,B,C cong X,Y,Z <=>
   A,B === X,Y /\ A,C === X,Z /\ B,C === Y,Z`;;

let is_ordered_DEF = new_definition
 `is_ordered (A,B,C,D) <=>
  B IN open_int (A,C) /\ B IN open_int (A,D) /\ C IN open_int (A,D) /\ C IN open_int (B,D)`;;

let Reflexive_relation_DEF = new_definition
  `Reflexive_Property <=> 
  !l A. Line l /\  ~(A IN l) ==> A,A same_side l`;;

let Symmetric_relation_DEF = new_definition
  `Symmetric_Property <=> 
  !l A B. Line l /\  ~(A IN l) /\ ~(B IN l) ==> 
  A,B same_side l ==> B,A same_side l`;;

let Transitive_relation_DEF = new_definition
  `Transitive_Property <=> 
  !l A B C. 
  Line l /\  ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==> 
  A,B same_side l /\ B,C same_side l ==> A,C same_side l`;;

(*
exec GOAL_TAC;
 p();; 

let Angle_DEF = new_definition
  `!A O B. Angle (A,O,B) = if Collinear (A,O,B) then {} else 
  {ray (O,A), ray (O,B)}`;;
*)

let InteriorAngle_DEF = new_definition
 `!A O B P. 
  P int_angle A,O,B <=> ~Collinear (A,O,B) /\ ?a b. 
  Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
  ~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b`;;


(* ------------------------------------------------------------------------- *)
(* The axioms.                                                               *)
(* ------------------------------------------------------------------------- *)

let I1 = new_axiom
  `!A B.  ~(A = B) ==> ?! l. Line l /\  A IN l /\ B IN l`;;

let I2 = new_axiom
  `!l. ? A B. Line l /\  A IN l /\ B IN l /\ ~(A = B)`;;

let I3 = new_axiom
  `?A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ 
                             ~Collinear (A,B,C)`;;

let B1 = new_axiom
  `! A B C. Between (A,B,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ 
            Between (C,B,A) /\ Collinear (A,B,C)`;;

let B2 = new_axiom
  `! A B. ~(A = B) ==> ?C. Between (A,B,C)`;;

let B3 = new_axiom
  `!A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear (A,B,C)
    ==> (Between (A,B,C) \/ Between (B,C,A) \/ Between (C,A,B)) /\
        ~(Between (A,B,C) /\ Between (B,C,A)) /\ 
        ~(Between (A,B,C) /\ Between (C,A,B)) /\ 
        ~(Between (B,C,A) /\ Between (C,A,B))`;;

let B4 = new_axiom
  `!l A B C. Line l /\ ~Collinear (A,B,C) /\ 
   ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\ 
   (?X. X IN l /\ Between (A,X,C)) ==> 
   (?Y. Y IN l /\ Between (A,Y,B)) \/ (?Y. Y IN l /\ Between (B,Y,C))`;;


let B1' = thm `;
  !A B C.  B IN open_int (A,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ 
             B IN open_int (C,A) /\ Collinear (A,B,C)
  by IN, Interval_DEF, B1`;;


let B2' = thm `;
  !A B. ~(A = B) ==> ?C.  B IN open_int (A,C)
  by IN, Interval_DEF, B2`;;


let B3' = thm `;
  !A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear (A,B,C)
    ==> (B IN open_int (A,C) \/ C IN open_int (B,A) \/ A IN open_int (C,B)) /\
        ~(B IN open_int (A,C) /\ C IN open_int (B,A)) /\ 
        ~(B IN open_int (A,C) /\ A IN open_int (C,B)) /\ 
        ~(C IN open_int (B,A) /\ A IN open_int (C,B))
  by IN, Interval_DEF, B3`;;


let B4' = thm `;
  let l be point_set;
  let A B C be point;
  assume Line l /\ ~Collinear (A,B,C) /\ 
   ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\ 
   (?X. X IN l /\  X IN open_int (A,C))		[H1];
   thus (?Y. Y IN l /\  Y IN open_int (A,B)) \/ (?Y. Y IN l /\  Y IN open_int (B,C))

   proof
     Line l /\ ~Collinear (A,B,C) /\ 
     ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\ 
     (?X. X IN l /\  Between (A,X,C)) by H1, IN, Interval_DEF;
     (?Y. Y IN l /\ Between (A,Y,B)) \/ (?Y. Y IN l /\ Between (B,Y,C)) by -, B4;
   qed by -, IN, Interval_DEF`;;

(*
What worked by B1, B2 and B3 doesn't work for B4:

let B4prime_THM = thm `;
  !l A B C. Line l /\ ~Collinear (A,B,C) /\ 
   ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) /\ 
   (?X. X IN l /\  X IN open_int (A,C)) ==>
   (?Y. Y IN l /\  Y IN open_int (A,B)) \/ (?Y. Y IN l /\  Y IN open_int (B,C)) 
   by B4, IN, Interval_DEF`;;

miz3 gives the error message #2:: 2: inference time-out
*)

let B4'' = thm `;
  let l be point_set;
  let A B C be point;
  assume Line l                                                         [H0];
  assume ~Collinear (A,B,C) /\ ~(A IN l) /\ ~(B IN l) /\ ~(C IN l)     [H1];
  assume A,B same_side l /\ B,C same_side l                             [H2];
  thus A,C same_side l

  proof 
   ~(?Y. Y IN l /\  Y IN open_int (A,B)) /\ 
   ~(?Y. Y IN l /\  Y IN open_int (B,C)) ==> 
   ~(?X. X IN l /\  X IN open_int (A,C))  by H0, H1, B4';
  qed by -, H1, H2, IN, same_side_DEF`;;


let BiggerThanSingleton_THM = thm `;
  let p be A->bool;
  let x be A;
  assume x IN p                                                         [H1];
  assume ~(p = {x})                                                     [H2];
  thus ?a . a IN p /\ ~(a = x)

  proof
     {x} SUBSET p by H1, SING_SUBSET;
    ~(p SUBSET {x}) by -,  H2, SUBSET_ANTISYM;
    consider a such that 
    a IN p /\ ~(a IN {x})                       [X1] by -, SUBSET;
     ~(a = x) by -, IN_SING;
  qed by -, X1`;;
 

let DisjointOneNotOther_THM = thm `;
  let x be A;
  let l m be A->bool;
  assume l INTER m = {}                                                 [H1];
  assume x IN m                                                         [H2];
  thus ~(x IN l)

  proof
    assume (x IN l);
    x IN l INTER m by -, H2, IN_INTER;
    F by -, NOT_IN_EMPTY, H1;
  qed by -`;;


let IntersectionSingletonOneNotOther_THM = thm `;
  let e x be A;
  let l m be A->bool;
  assume l INTER m = {x}                                                [H1];
  assume e IN l                                                         [H2];
  assume ~(e = x)                                                       [H3];
  thus ~(e IN m)

  proof
    assume e IN m;
    e IN l INTER m by H2, -, IN_INTER;
    e = x by -, H1, IN_SING;
    F by -, H3;
  qed by -`;;


let EquivIntersectionHelp_THM = thm `;
  let a x be A;
  let l m be A->bool;
  assume l INTER m = {x}                                                [H1];
  assume a IN m DELETE x                                                [H2];
  thus ~(a IN l) 

  proof
    a IN m /\ ~(a = x)                          [X1] by H2, IN_DELETE;
    qed by -, H1, H2, IntersectionSingletonOneNotOther_THM`;;


let DoubleSubsetEqual_THM = thm `;
  let s t be A->bool;
  assume s SUBSET t                     [H1];
  assume t SUBSET s                     [H2];
  thus s = t

  proof
   !x:A. x IN s ==> x IN t [sSt] by H1, SUBSET;
   !x:A. x IN t ==> x IN s [tSs] by H2, SUBSET;
   !x:A. x IN s <=> x IN t [sEt] by sSt, tSs;
   s = t by -, EXTENSION;
  qed by -`;;


let SubsetTensor_THM = thm `;
  let a b s be A->bool;
  assume a SUBSET b [H1];
  thus a INTER s SUBSET b INTER s /\ 
  s INTER a SUBSET s INTER b

  proof
    a INTER s SUBSET s /\ s INTER a SUBSET s     [asa_s] by INTER_SUBSET;
    a INTER s SUBSET a /\ s INTER a SUBSET a      by INTER_SUBSET;
    a INTER s SUBSET b /\ s INTER a SUBSET b      by -, H1, SUBSET_TRANS;
  qed by -, asa_s, SUBSET_INTER`;;


let NonemptySubsetSing_THM = thm `;
  let a be A;
  let l be A->bool;
  assume ~(l = {}) [H1];
  assume l SUBSET {a} [H2];
  thus a IN l

  proof
    consider x such that 
    x IN l [xl] by H1, MEMBER_NOT_EMPTY;
    x IN {a} by -, H2, SUBSET;
    x = a by -, IN_SING;
  qed by -, xl`;;


let CollinearSymmetry_THM = thm `;
  let A B C be point;
  assume Collinear (A,B,C)                    [H1];
  thus Collinear (A,C,B) /\ Collinear (B,A,C) /\ Collinear (B,C,A) /\ 
       Collinear (C,A,B) /\ Collinear (C,B,A) 

  proof
    consider l such that 
    Line l /\ A IN l /\ B IN l /\ C IN l by H1, Collinear_DEF;
  qed by -, Collinear_DEF`;;


let OnePointImpliesAnother_THM = thm `;
  let P be point; 
  thus ?Q:point. ~(Q = P)

  proof
    consider A B C such that 
    ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear (A,B,C) [X1] by I3;
    cases;
    suppose B = P;
      ~(A = B) by -, X1;
    qed by -;
    suppose ~(B = P);
    qed by -;
  end`;;


let ExistsPointOffLine_THM = thm `;
  let l be point_set; 
  assume Line l                                                         [H1];
  thus ?Q:point. ~(Q IN l)

  proof
    consider A B C such that 
    ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear (A,B,C) [useI3] by I3;
    cases;
    suppose ~(A IN l) \/ ~(B IN l) \/ ~(C IN l);
    qed by -;
    suppose (A IN l) /\ (B IN l) /\ (C IN l);
      Collinear (A,B,C) by H1, -, Collinear_DEF;
      F by -, useI3;
    qed by -;
  end`;;


let BetweenLinear_THM = thm `;
  let A B C be point;
  let m be point_set;
  assume Line m /\ A IN m /\ C IN m                                     [H1];
  assume B IN open_int (A,C) \/ C IN open_int (B,A)  \/ A IN open_int (C,B)      [H2];
  thus B IN m

  proof
    ~(A = C) /\ 
    (Collinear (A,B,C) \/ Collinear (B,C,A) \/ Collinear (C,A,B))  [X1] by H2, B1';
    consider l such that
    Line l /\ A IN l /\ B IN l /\ C IN l              [X2] by -, Collinear_DEF;
    l = m by X1, -, H2, H1, I1;
  qed by -, X2`;;

 
let CollinearLinear_THM = thm `;
  let A B C be point;
  let m be point_set;
  assume Line m /\ A IN m /\ C IN m                                     [H1];
  assume Collinear (A,B,C) \/ Collinear (B,C,A) \/ Collinear (C,A,B)       [H2];
  assume ~(A = C)                                                       [H3];
  thus B IN m

  proof
    consider l such that 
    Line l /\ A IN l /\ B IN l /\ C IN l           [X1] by H2, Collinear_DEF;
    l = m by H3, -, H1, I1;
  qed by -, X1`;;
 

let NonCollinearImpliesDistinct_THM = thm `;
  let A B C be point;
  assume ~Collinear (A,B,C)                                            [H1];
  thus ~(A = B) /\ ~(A = C) /\ ~(B = C)

  proof
    cases;
    suppose A = B /\ B = C                                              [C1];
      consider Q such that ~(Q = A) by OnePointImpliesAnother_THM;
      consider l such that Line l /\ A IN l /\ Q IN l by -, I1;
      Collinear (A,B,C) by -, C1, Collinear_DEF;
    qed by -, H1;
    suppose ~(A = B) /\ B = C                                           [C2];
      consider l such that Line l /\ A IN l /\ B IN l by -, I1;
      Collinear (A,B,C) by -, C2, Collinear_DEF;
    qed by -, H1;
    suppose ~(B = C)                                                    [C3];
      consider l such that Line l /\ B IN l /\ C IN l [X1] by C3, I1;
      ~(A = B)                                                          [U] 
      proof
        assume A = B;
        Collinear (A,B,C) by -, X1, Collinear_DEF;
      qed by -, H1; 
      ~(A = C)                                                          [V]
      proof
        assume A = C;
        Collinear (A,B,C) by -, X1, Collinear_DEF;
      qed by -, H1; 
    qed by U, V, C3;          
  end`;;


let OpenIntervalSubsetLine_THM = thm `;
  let A B be point;
  let l be point_set;
  assume Line l /\ A IN l /\ B IN l     [H1];
  thus open_int (A,B) SUBSET l

  proof
    !X. X IN open_int (A,B) ==> X IN l
    proof
      let X be point;
      assume X IN open_int (A,B);
    qed     by -, H1, BetweenLinear_THM;
  qed     by -, SUBSET`;;


let Reverse4Order_THM = thm `;
  let A B C D be point;
  assume is_ordered (A,B,C,D) [H1];
  thus is_ordered (D,C,B,A)

  proof
    B IN open_int (A,C) /\ B IN open_int (A,D) /\ 
    C IN open_int (A,D) /\ C IN open_int (B,D) by H1, is_ordered_DEF;
    B IN open_int (C,A) /\ B IN open_int (D,A) /\ 
    C IN open_int (D,A) /\ C IN open_int (D,B) by -, B1';
  qed by -, is_ordered_DEF`;;


let OriginInRay_THM = thm `;
  let O Q be point;
  assume ~(Q = O)                               [H1];
  thus O IN ray (O,Q)

  proof
    ~(O IN open_int (O,Q)) [OOQ] by B1';
    consider l such that 
    Line l /\ O IN l /\ Q IN l by H1, I1;
    Collinear (O,Q,O) by -, Collinear_DEF;
  qed by H1, -, OOQ, IN, Ray_DEF`;;


let EndpointInRay_THM = thm `;
  let O Q be point;
  assume ~(Q = O)                               [H1];
  thus Q IN ray (O,Q)

  proof
    ~(O IN open_int (Q,Q)) [notOQQ] by B1';
    consider l such that 
    Line l /\ O IN l /\ Q IN l by H1, I1;
    Collinear (O,Q,Q) by -, Collinear_DEF;
  qed by H1, -, notOQQ, IN, Ray_DEF`;;


let Line01infinity_THM = thm `;
  let X be point;
  let l m be point_set;
  assume Line l /\ Line m                                               [H0];
  assume ~(l = m)                                                       [H1];
  assume X IN l /\ X IN m                                               [H2];
  thus l INTER m = {X}

  proof
    assume ~(l INTER m = {X})                                           [H3];
    X IN l INTER m by H2, IN_INTER;
    consider A such that
    A IN l INTER m  /\ ~(A = X)         [X1] by -, H3, BiggerThanSingleton_THM;
    A IN l /\ X IN l /\ A IN m /\ X IN m by H0, -, H2, IN_INTER;
    l = m by H0, -, X1, I1;
    F by -, H1;
  qed by -`;;
 

let EquivIntersection_THM = thm `;
  let A B X be point;
  let l m be point_set;
  assume Line l /\ Line m                                               [H0];
  assume l INTER m = {X}                                                [H1];
  assume A IN m DELETE X /\ B IN m DELETE X                             [H2];
  assume ~(X IN open_int (A,B))                                         [H3];
  thus  ~(A IN l) /\ ~(B IN l) /\ A,B same_side l

  proof
    A IN m /\ ~(A = X)                          [X1] by H2, IN_DELETE;
    B IN m /\ ~(B = X)                          [X2] by H2, IN_DELETE;
    ~(A IN l) /\ ~(B IN l) [X3] by H1, H2, EquivIntersectionHelp_THM;
    A,B same_side l                                                     [X4]
    proof
      assume ~(A,B same_side l);
      consider G such that 
      (G IN l) /\ G IN open_int (A,B)           [X5] by H0, -, same_side_DEF;
      
       ~(A = B) /\ Collinear (A,G,B)            [X6] by -, B1';
      consider k such that 
      Line k /\ A IN k /\ G IN k /\ B IN k      [X7] by -, Collinear_DEF;
      k = m by H0, -, X1, X2, X6, I1;
      G IN l INTER m by -, X5, X7, IN_INTER;
      G = X by -, H1, IN_SING;
      X IN open_int (A,B) by -, X5;
      F by -, H3;
    qed by -;
  qed by X3, X4`;;


let SameSideReflexiveRelation_THM = thm `;
  thus Reflexive_Property

  proof
    !l A. Line l ==>  A,A same_side l
    proof
      let l be point_set;
      let A be point;
      assume Line l                                                     [H0];
       ~(?X. (X IN l) /\ X IN open_int (A,A)) by H0, B1';
    qed by H0, -, same_side_DEF;
  qed by -, Reflexive_relation_DEF`;;


let SameSideSymmetricRelation_THM = thm `;
  thus Symmetric_Property

  proof
    !l A B. Line l /\ ~(A IN l) /\ ~(B IN l) ==> 
    A,B same_side l ==> B,A same_side l
    proof
      let l be point_set;
      let A B be point;
      assume Line l                                                     [H0];
      assume A,B same_side l                                            [H1];
      assume ~(A IN l) /\ ~(B IN l);
      ~(?X. (X IN l) /\ X IN open_int (A,B)) by H0, H1, same_side_DEF;
      ~(?X. (X IN l) /\ X IN open_int (B,A)) by -, B1';
    qed by H0, -, same_side_DEF;
  qed by -, Symmetric_relation_DEF`;;


let SameSideTransitiveRelation_THM = thm `;
  thus Transitive_Property

  proof
    !l A B C. 
    Line l /\ ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==> 
    A,B same_side l /\ B,C same_side l ==> A,C same_side l 
    proof
      let l be point_set;
      let A B C be point;
      assume Line l                                                     [lLine];
      assume ~(A IN l) /\ ~(B IN l) /\ ~(C IN l)                        [H0];
      assume A,B same_side l                                            [H1];
      assume B,C same_side l                                            [H2];
      A,C same_side l
      proof
        ~Collinear (A,B,C) \/ Collinear (A,B,C);
        cases by -;
        suppose ~Collinear (A,B,C);
        qed by lLine, -, H0, H1, H2, B4'';
        suppose Collinear (A,B,C)                                      [Coll];
          cases;
          suppose A = B \/ A = C \/ B = C;
          qed by lLine, -, H2, H0, SameSideReflexiveRelation_THM, 
                            Reflexive_relation_DEF, H1;
          suppose ~(A = B) /\ ~(A = C) /\ ~(B = C)      [Distinct];
            consider m such that 
            Line m /\ A IN m /\ C IN m                  [ACm] by Distinct, I1;
            ~(l = m)                                    [not_lm] by ACm, H0;
            cases;
            suppose l INTER m = {}                      [Disjoint];
              !X. X IN open_int (A,C) ==> ~(X IN l)
              proof
                let X be point;
                assume X IN open_int (A,C);
                X IN m by lLine, -, ACm, BetweenLinear_THM;
                ~(X IN l) by -, Disjoint, DisjointOneNotOther_THM; 
              qed by -;
            qed by lLine, -, same_side_DEF;
            suppose ~(l INTER m = {})                   [NotDisjoint];
              consider X such that
              X IN l INTER m by NotDisjoint, MEMBER_NOT_EMPTY;
              X IN l /\ X IN m                          [Xin_lm] by -, IN_INTER;
              l INTER m = {X}           [lmX] by lLine, ACm, not_lm, -, Line01infinity_THM;
              consider E such that 
              E IN l /\ ~(E = X)                        [Einl_X] by Xin_lm, I2;
              ~(E IN m) [notEm] by lmX, Einl_X, IntersectionSingletonOneNotOther_THM;
              ~(E = B) by Einl_X, H0;
              consider B' such that 
              B IN open_int (E,B') by -, B2';
              B IN open_int (B',E)                         [B'BE] by -, B1';
              ~(B' = E) /\ ~(B = E) /\ ~(B' = B) /\ Collinear (B',B,E) [B'BEcol] by -, B1';
              consider n such that 
              Line n /\ E IN n /\ B' IN n               [EB'n] by -, I1;
              B IN n                    [Bn] by EB'n, B'BE, BetweenLinear_THM;
              ~(l = n)                  [not_ln] by H0, -;
              l INTER n = {E} [lnE] by lLine, not_ln, EB'n, Einl_X, Line01infinity_THM;
              ~(B' IN l) [notB'l] by -, EB'n, B'BEcol, IntersectionSingletonOneNotOther_THM;
              ~(E IN open_int (B,B'))        [BEB'] by B'BEcol, B'BE, B3';
              B' IN n DELETE E /\ B IN n DELETE E by EB'n, Bn, B'BEcol, IN_DELETE;
              B, B' same_side l [Bsim_lB'] by lLine, EB'n, lnE, -, BEB', EquivIntersection_THM;
              ~(m = n)                   [not_mn] by  EB'n, notEm;
              B IN m by ACm, Coll, Distinct, CollinearLinear_THM;
              m INTER n = {B} [mn_B]  by ACm, EB'n, -, Bn, not_mn, Line01infinity_THM;
              ~(A IN n) [not_An] by -, ACm, Distinct, IntersectionSingletonOneNotOther_THM;
              ~Collinear (A,B,B')
              proof
                assume Collinear (A,B,B');
                consider alpha such that 
                Line alpha /\ A IN alpha /\ B IN alpha /\ B' IN alpha [ABB'alpha] by -, Collinear_DEF;
                alpha = n by B'BEcol, ABB'alpha, EB'n, Bn, I1;
                A IN n by -, ABB'alpha;
              qed by -, not_An;
              A,B' same_side l          [Asim_lB'] by lLine, -, H0, notB'l, H1, Bsim_lB', B4'';

              ~(C IN n)                 [notCn] by mn_B, ACm, Distinct, 
              IntersectionSingletonOneNotOther_THM;
              C,B same_side l [Csim_lB] by lLine, H0, H2, SameSideSymmetricRelation_THM, 
              Symmetric_relation_DEF;
              ~Collinear (C,B,B')
              proof
                assume Collinear (C,B,B');
                consider alpha such that 
                Line alpha /\ C IN alpha /\ B IN alpha /\ B' IN alpha [CBB'alpha] by -, Collinear_DEF;
                alpha = n by -, EB'n, B'BEcol, CBB'alpha, Bn, I1;
                C IN n by -, CBB'alpha;
              qed by -, notCn;
              C,B' same_side l by lLine, -, H0, notB'l, Csim_lB, Bsim_lB', B4'';
              B',C same_side l [B'sim_C] by lLine, H0, notB'l, -, SameSideSymmetricRelation_THM, 
              Symmetric_relation_DEF;
              ~(B' IN m) [notB'm] by mn_B, EB'n, B'BEcol, IntersectionSingletonOneNotOther_THM;
              ~Collinear (A,B',C) 
              proof
                assume Collinear (A,B',C);
                consider alpha such that 
                Line alpha /\ A IN alpha /\ B' IN alpha /\ C IN alpha [AB'Calpha] by -, Collinear_DEF;
                alpha = m by Distinct, -, ACm, I1;
                B' IN m by -, AB'Calpha;
                F by -, notB'm;
              qed by -;
              A, C same_side l by lLine, -, H0, notB'l, Asim_lB', B'sim_C, B4'';
            qed by -;
          end;
        end;
      end;
    qed by -;
  qed by -, Transitive_relation_DEF`;;


let SameSideEquivalenceRelation_THM = thm `;
  thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
  proof
  qed by SameSideReflexiveRelation_THM, SameSideSymmetricRelation_THM,
  SameSideTransitiveRelation_THM`;;


let ConverseCrossbar_THM = thm `;
  let O A B G be point;
  assume ~Collinear (A,O,B)                                            [H1];
  assume G IN open_int (A,B)                                               [H2];
  thus G int_angle A,O,B

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, 
                                                 NonCollinearImpliesDistinct_THM;
    consider a such that Line a /\ O IN a /\ A IN a                         [aOA] by -, I1;
    consider b such that Line b /\ O IN b /\ B IN b                  [bOB] by Distinct, I1;
    consider l such that Line l /\ A IN l /\ B IN l                  [lAB] by Distinct, I1;
     ~(B IN a) by H1, aOA, Collinear_DEF;
    ~(a = l) by -, lAB;
    a INTER l = {A}                     [alA] by -, aOA, lAB, Line01infinity_THM;
    ~(A = G) /\ ~(A = B) /\ ~(G = B) /\  G IN open_int (B,A) /\ Collinear (A,G,B) 
                                                                  [X1] by H2, B1';
    ~(A IN open_int (G,B))                                 [notGAB] by -, H2, B3', B1';
    G IN l                                  [Ginl] by lAB, H2, BetweenLinear_THM;
   ~(G IN a)    [notGina] by alA, Ginl, X1, IntersectionSingletonOneNotOther_THM;
    G IN l DELETE A /\ B IN l DELETE A by Ginl, lAB, X1, IN_DELETE;
    G,B same_side a           [Gsim_aB] by aOA, lAB, alA, -, notGAB, EquivIntersection_THM;
    :: same argument shows   G,A same_side b
    ~(A IN b) by H1, bOB, Collinear_DEF;
    ~(b = l) by -, lAB;
    b INTER l = {B}                     [blB] by -, bOB, lAB, Line01infinity_THM;
    ~(B IN open_int (G,A))              [notGBA] by H2, B1', B3';   
    ~(G IN b)   [notGinb] by blB, Ginl, X1, IntersectionSingletonOneNotOther_THM;
    G IN l DELETE B /\ A IN l DELETE B by Ginl, lAB, X1, IN_DELETE;
    G,A same_side b            [Gsim_bA] by bOB, lAB, blB, -, notGBA, EquivIntersection_THM;
  qed by H1, aOA, bOB, notGina, notGinb, Gsim_aB, Gsim_bA, InteriorAngle_DEF`;;


let InteriorHelp_THM = thm `;
  let A O B P be point;
  let a b be point_set;
  assume Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b       [aOAbOB];
  assume  P int_angle A,O,B                                             [P_AOB];
  thus ~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b

  proof
    consider alpha beta such that ~Collinear (A,O,B) /\ 
    Line alpha /\ O IN alpha /\ A IN alpha /\ 
    Line beta /\ O IN beta /\B IN beta /\
    ~(P IN alpha) /\ ~(P IN beta) /\ 
    P,B same_side alpha /\ P,A same_side beta [exists] by P_AOB, InteriorAngle_DEF;
    ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by -, NonCollinearImpliesDistinct_THM;
    alpha = a /\ beta = b by -, aOAbOB, exists, I1;
  qed by -, exists`;;


let InteriorEZHelp_THM = thm `;
  let A O B P be point;
  assume  P int_angle A,O,B                                             [P_AOB];
  thus ~(P = A) /\ ~(P = O) /\ ~(P = B) /\ ~Collinear (A,O,P) 

  proof
    consider a b such that 
    ~Collinear (A,O,B) /\
    Line a /\ O IN a /\ A IN a /\ 
    Line b /\ O IN b /\B IN b /\
    ~(P IN a) /\ ~(P IN b)     [def_int] by P_AOB, InteriorAngle_DEF;
    ~(P = A) /\ ~(P = O) /\ ~(P = B)     [PnotAOB] by -;
    ~(A = O)     [notAO] by def_int, NonCollinearImpliesDistinct_THM;
    ~Collinear (A,O,P)
    proof
      assume Collinear (A,O,P);
      consider l such that 
      Line l /\ A IN l /\ O IN l /\ P IN l     [lAOP] by -, Collinear_DEF;
      l = a     by notAO, -, def_int, I1;
      (P IN a)     by -, lAOP;
    qed by -, def_int;
  qed by PnotAOB, -`;;


let WholeRayInterior_THM = thm `;
  let A O B X P be point;
  assume ~Collinear (A,O,B)                                            [H1];
  assume X int_angle A,O,B                                              [H2];
  assume P IN ray (O,X)                                                  [H3];
  assume ~(P = O)                                                       [H4];
  thus P int_angle A,O,B

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct_THM;
    consider a such that Line a /\ O IN a /\ A IN a       [a_OA] by Distinct, I1;
    consider b such that Line b /\ O IN b /\ B IN b       [b_OB] by Distinct, I1;
    ~(X IN a) /\ ~(X IN b) /\ X,B same_side a /\ X,A same_side b [XintAOB] by H2, a_OA, b_OB, InteriorHelp_THM; 
    ~(O = X) /\ Collinear (O,X,P) /\ ~(O IN open_int (P,X)) [P_OX] by H3, IN, Ray_DEF;
    consider x such that Line x /\ O IN x /\ X IN x       [x_OX] by P_OX, I1;
    :: P IN x       [Pin_x] by x_OX, P_OX, Collinear_DEF, CollinearLinear_THM;
    P IN x       [Pin_x] by x_OX, P_OX, CollinearLinear_THM;
    P IN x DELETE O                         [Pin_x_O] by Pin_x, H4, IN_DELETE;
    X IN x DELETE O                    [Xin_x_O] by x_OX, P_OX,  IN_DELETE;
    ~(x = a) /\ ~(x = b)               [x_not_ab] by XintAOB, x_OX;
    a INTER x = {O} /\ b INTER x = {O} [axb_intO] by x_not_ab, x_OX, a_OA, b_OB, Line01infinity_THM;
    ~(P IN a) /\ P,X same_side a [Psim_aX] by a_OA, x_OX, axb_intO, Pin_x_O, Xin_x_O, P_OX, EquivIntersection_THM;
    ~(P IN b) /\ P,X same_side b [Psim_bX] by b_OB, x_OX, axb_intO, Pin_x_O, Xin_x_O, P_OX, EquivIntersection_THM;
    P,B same_side a  /\ P,A same_side b by Psim_aX, Psim_bX, XintAOB, a_OA, b_OB, H1, Collinear_DEF, SameSideTransitiveRelation_THM, Transitive_relation_DEF;
  qed by H1, a_OA, b_OB, Psim_aX, Psim_bX, -, InteriorAngle_DEF`;;


let AngleOrdering_THM = thm `;
  let O A P Q be point;
  let a be point_set;
  assume ~(O = A)                                                       [H1];
  assume Line a /\ O IN a /\ A IN a                                               [H2];
  assume ~(P IN a) /\ ~(Q IN a)                                         [H3];
  assume P, Q same_side a                                               [H4];
  assume ~Collinear (P,O,Q)                                            [H5];
  thus P int_angle Q,O,A \/ Q int_angle P,O,A

  proof
    ~(P = O) /\ ~(P = Q) /\ ~(O = Q) [Distinct] by H5, NonCollinearImpliesDistinct_THM;
    consider p such that Line p /\ O IN p /\ P IN p             [p_OP] by Distinct, I1;
    consider q such that Line q /\ O IN q /\ Q IN q             [q_OQ] by Distinct, I1;
    ~(q = a) by H3, q_OQ;
    q INTER a = {O}                       by -, H2, q_OQ, Line01infinity_THM;
    ~(A IN q) by -, H2, H1, IntersectionSingletonOneNotOther_THM;
    ~(P IN q)                             [notPq] by q_OQ, H5, Collinear_DEF;
    ~(p = q) by -, p_OP;
    p INTER q = {O}                     by -, p_OP, q_OQ, Line01infinity_THM;
    ~Collinear (Q,O,A)        [QOA_noncol] by H1, H2, I1, H3, Collinear_DEF;
    ~Collinear (P,O,A)         [POA_noncol] by H1, H2, I1, H3, Collinear_DEF;

    assume ~(P int_angle Q,O,A)                                   [notP_QOA];
    Q int_angle P,O,A
    proof
      ~(P,A same_side q)                        by QOA_noncol, H2, q_OQ, H3,
                                      notPq, H4, notP_QOA, InteriorAngle_DEF;
      consider G such that (G IN q) /\ G IN open_int (P,A) [existG] by q_OQ, -, same_side_DEF;
      G int_angle P,O,A [G_POA] by  POA_noncol, existG, ConverseCrossbar_THM;
      ~(G IN a) /\ G,P same_side a [Gsim_aP] by -, InteriorAngle_DEF, H1, H2, I1;
      ~(G = O)                     [GnotO] by -, H2;
      G,Q same_side a              by H2, Gsim_aP, H3, H4, 
                      SameSideTransitiveRelation_THM, Transitive_relation_DEF;
      ~(O IN open_int (Q,G))       [notQOG] by -, same_side_DEF, H2, B1';
      Collinear (O,G,Q)             by q_OQ, existG, Collinear_DEF; 
      Q IN ray (O,G) by GnotO, -, notQOG, IN, Ray_DEF;
    qed by POA_noncol, G_POA, -, Distinct, WholeRayInterior_THM;
  qed by -`;;


let InteriorReflectionInterior_THM = thm `;
  let A O B D A' be point;
  assume ~Collinear (A,O,B)                                            [H1];
  assume D int_angle A,O,B                                              [H2];
  assume O IN open_int (A,A')                                              [H3];
  thus B  int_angle D,O,A'

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct_THM;
    consider a such that 
    Line a /\ O IN a /\ A IN a                                  [a_OA] by Distinct, I1;
    consider b such that 
    Line b /\ O IN b /\ B IN b                                [b_OB] by Distinct, I1;
    ~(A IN b)                             [notAb] by b_OB, H1, Collinear_DEF;
    ~(B IN a)                             [notBa] by a_OA, H1, Collinear_DEF;
   ~(a = b) by -, b_OB;
    b INTER a = {O}              [ab_O] by -, a_OA, b_OB, Line01infinity_THM;
    A' IN a                      [A'a] by H3, a_OA, BetweenLinear_THM;
    A' IN a DELETE O by A'a, H3, B1', IN_DELETE; 
    ~(A' IN b)                [notA'b] by ab_O, -, EquivIntersectionHelp_THM;
    ~(A,A' same_side b)       [Ansim_bA'] by b_OB, H3, same_side_DEF ;
    ~(D IN a) /\ ~(D IN b) /\ 
    D,B same_side a /\ D,A same_side b [DintAOB] by a_OA, b_OB, H2, InteriorHelp_THM;
    ~(D,A' same_side b)       [Dnsim_bA']
    proof
      assume D,A' same_side b;
      A',D same_side b by b_OB, DintAOB, notA'b, -, SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
      A',A same_side b by b_OB, DintAOB, notA'b, notAb, -, SameSideTransitiveRelation_THM, Transitive_relation_DEF;                       
      A,A' same_side b by b_OB, notA'b, notAb, -, SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
      F by -, Ansim_bA';
    qed by -;
    ~(D int_angle B,O,A')                                       [notD_BOA']
    proof
      assume D int_angle B,O,A';
      D,A' same_side b by b_OB, a_OA, A'a, -, DintAOB, InteriorHelp_THM;
      F by -, Dnsim_bA';     
    qed by -; 
    ~Collinear (D,O,B) [DOB_noncol] by Distinct, b_OB, I1, DintAOB, Collinear_DEF;
    ~(O = A') by H3, B1';
    B int_angle D,O,A' by -, a_OA, A'a, DintAOB, notBa, DOB_noncol, notD_BOA', AngleOrdering_THM;
  qed by -`;;


let Crossbar_THM = thm `;
  let O A B D be point;
  assume ~Collinear (A,O,B)                                             [H1];
  assume D int_angle A,O,B                                              [H2];
  thus ?G. G IN open_int (A,B) /\ G IN ray (O,D) DELETE O

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B)     [Distinct] by H1, NonCollinearImpliesDistinct_THM;
    consider a such that 
    Line a /\ O IN a /\ A IN a                                  [a_OA] by Distinct, I1;
    consider b such that 
    Line b /\ O IN b /\ B IN b                                  [b_OB] by Distinct, I1;
    ~(B IN a)     [notBa] by a_OA, H1, Collinear_DEF;
    ~(D IN a) /\ ~(D IN b) /\ D,B same_side a [D_AOB] by a_OA, b_OB, H2, InteriorHelp_THM;
    ~(D = O)                                          	       	[DnotO] by D_AOB, a_OA;
    consider l such that 
    Line l /\ O IN l /\ D IN l                                  [l_OD] by -, I1;
    ~(a = l) /\ ~(b = l)     [abl_distinct] by l_OD, D_AOB, b_OB, notBa;
    a INTER l = {O} /\ b INTER l = {O}     [ablO] by abl_distinct, a_OA, b_OB, l_OD, Line01infinity_THM; 
    ~(A IN l) /\ ~(B IN l)     [ABnot_l] by -, a_OA, b_OB, Distinct, IntersectionSingletonOneNotOther_THM;
    consider A' such that 
    O IN open_int (A,A')     [AOA'] by Distinct, B2';
    A' IN a     [A'a] by a_OA, -, BetweenLinear_THM;
    ~(A' = O)     by AOA', B1';
    ~(A' IN l)     [A'not_l] by ablO, A'a, -, IntersectionSingletonOneNotOther_THM;
    ~(A,A' same_side l)     [Ansim_lA'] by l_OD, AOA', same_side_DEF;

    B int_angle D,O,A'     by H1, H2, AOA', InteriorReflectionInterior_THM;
    B,A' same_side l     [Bsim_lA'] by l_OD, a_OA, A'a, -, InteriorHelp_THM;
    ~(A,B same_side l)     [Ansim_lB]
    proof
      assume A,B same_side l;
      A,A' same_side l     by l_OD, ABnot_l, A'not_l, -, Bsim_lA', SameSideTransitiveRelation_THM, Transitive_relation_DEF;
    qed by -, Ansim_lA';
    consider G such that 
    G IN open_int (A,B) /\ G IN l             [AGB] by l_OD, Ansim_lB, same_side_DEF;
    Collinear (O,D,G)                         [ODGcol] by AGB, l_OD, Collinear_DEF;
    G int_angle A,O,B                         by H1, AGB, ConverseCrossbar_THM;
    ~(G IN a) /\ G,B same_side a     [Gsim_aB] by a_OA, b_OB, -, InteriorHelp_THM;
    ~(G = O) [GnotO]     by -, a_OA;
    D,B same_side a     by a_OA, b_OB, H2, InteriorHelp_THM;
    B,D same_side a     by a_OA, notBa, D_AOB, -, SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
    G,D same_side a     [Gsim_aD] by a_OA, Gsim_aB, notBa, D_AOB, Gsim_aB, -, SameSideTransitiveRelation_THM, Transitive_relation_DEF;
    ~(O IN open_int (G,D))     by a_OA, -, same_side_DEF;
    G IN ray (O,D)     [G_OD] by DnotO, ODGcol, -, IN, Ray_DEF;
    G IN ray (O,D) DELETE O     by -, GnotO, IN_DELETE;
  qed by AGB, -`;;


let IntervalTransitivity_THM = thm `;
  let O P Q R be point;
  let m be point_set;
  assume Line m                                                         [H0];
  assume O IN m                                                         [H1];
  assume P IN m DELETE O /\ Q IN m DELETE O /\ R IN m DELETE O          [H2];
  assume ~(O IN open_int (P,Q)) /\ ~(O IN open_int (Q,R))               [H3];
  thus ~(O IN open_int (P,R))

  proof
    P IN m /\ Q IN m /\ R IN m /\ ~(P = O) /\ ~(Q = O) /\ ~(R = O) [H2'] by H2, IN_DELETE;
    consider E such that 
    ~(E IN m)                            [notEm] by H0, ExistsPointOffLine_THM;
    ~(O = E) by H1, notEm;
    consider l such that 
    Line l /\ O IN l /\ E IN l                   [OE_l] by -, I1;
    ~(m = l) by notEm, OE_l;
    l INTER m = {O}                      [ml_O] by OE_l, H0, -, H1, OE_l, Line01infinity_THM;
    ~(P IN l) /\  ~(Q IN l) /\ ~(R IN l) [PQRnotl] by ml_O, H2', IntersectionSingletonOneNotOther_THM;
    P,Q same_side l /\ Q,R same_side l   [Psim_lQsim_lR] by OE_l, H0, ml_O, H2, H3, PQRnotl, EquivIntersection_THM;
    P,R same_side l                      [Psim_lR] by OE_l, PQRnotl, Psim_lQsim_lR, 
                                         SameSideTransitiveRelation_THM, Transitive_relation_DEF;
  qed by OE_l, -, same_side_DEF`;;


let RayLine_THM = thm `;
  let O P be point;
  let l be point_set;
  assume Line l /\ O IN l /\ P IN l                     [H1];
  thus ray (O,P)  SUBSET l

  proof
    !X. X IN ray (O,P)  ==> X IN l 
    proof
      let X be point;
      assume X IN ray (O,P);
      ~(O = P) /\ Collinear (O,P,X)     by -, IN, Ray_DEF;
      X IN l by H1, -, CollinearLinear_THM;
      qed by -;
    qed by -, SUBSET`;;


let RayWellDefinedHalfway_THM = thm `;
  let O P Q be point;
  assume ~(Q = O)                               [H1];
  assume P IN ray (O,Q) DELETE O                 [H2];
  thus ray (O,P) SUBSET ray (O,Q)

  proof
    consider m such that 
    Line m /\ O IN m /\ Q IN m     [OQm] by H1, I1;
    P IN ray (O,Q) /\ ~(P = O)     [H2'] by H2, IN_DELETE;
    P IN m     [Pm] by OQm, H2', RayLine_THM, SUBSET;
    P IN m DELETE O /\ Q IN m DELETE O [PQm_O] by Pm, H2', OQm, H1, IN_DELETE;
    ~(O IN open_int (P,Q))     [notPOQ] by H2', IN, Ray_DEF;
    !X. X IN ray (O,P) ==> X IN ray (O,Q)
    proof
      let X be point;
      assume X IN ray (O,P)     [XrOP];
      X IN m     [Xm] by OQm, Pm, H2', -, RayLine_THM, SUBSET;
      Collinear (O,Q,X)     [OQXcol] by OQm, Xm,  Collinear_DEF;
      ~(O IN open_int (X,P))     [notXOP] by XrOP, IN, Ray_DEF;
      cases;
      suppose X = O;
        X IN ray (O,Q) by H1, -, OriginInRay_THM;
      qed by -;
      suppose ~(X = O) [notXO];
        X IN m DELETE O by Xm, notXO, IN_DELETE;
        ~(O IN open_int (X,Q)) by OQm, -, PQm_O, notXOP, notPOQ, IntervalTransitivity_THM;  
        X IN ray (O,Q) by H1, OQXcol, -, IN, Ray_DEF;
      qed by -;
    end;
  qed by -, SUBSET`;;


let RayWellDefined_THM = thm `;
  let O P Q be point;
  assume ~(Q = O)                                                       [H1];
  assume P IN ray (O,Q) DELETE O                                        [H2];
  thus ray (O,P) = ray (O,Q)

  proof
    ray (O,P) SUBSET ray (O,Q)     [PsubsetQ] by H1, H2, RayWellDefinedHalfway_THM; 
    P IN ray (O,Q) /\ ~(P = O)     [H2'] by H2, IN_DELETE;
    Collinear (O,Q,P) /\ ~(O IN open_int (P,Q))     [notPOQ] by H2', IN, Ray_DEF;
    Collinear (O,P,Q)     [OQPcol] by notPOQ, CollinearSymmetry_THM;
    ~(O IN open_int (Q,P))     [notQOP] by notPOQ, B1';
    Q IN ray (O,P) by H2', OQPcol, notQOP, IN, Ray_DEF;
    Q IN ray (O,P) DELETE O [QrOP_O] by -, H1, IN_DELETE;
    ray (O,Q) SUBSET ray (O,P)     [QsubsetP] by H2', QrOP_O, RayWellDefinedHalfway_THM; 
  qed by PsubsetQ, QsubsetP, DoubleSubsetEqual_THM `;;


let OppositeRaysIntersect1pointHelp_THM = thm `;
  let A O B X be point;
  assume O IN open_int (A,B)                                                       [H1];                   
  assume X IN ray (O,B) DELETE O     [H2];
  thus ~(X IN ray (O,A))

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B) /\ Collinear (A,O,B) [B1_AOB] by H1, B1';
    X IN ray (O,B) /\ ~(X = O)     [H2'] by H2, IN_DELETE; 
    Collinear (O,B,X) /\ ~(O IN open_int (X,B))     [K2] by -, IN, Ray_DEF;
    consider m such that
    Line m /\ A IN m /\ B IN m     [ABm] by B1_AOB, I1;
    O IN m     [Om] by ABm, B1_AOB, CollinearLinear_THM;
    X IN m     [Xm] by ABm, Om, K2, B1_AOB, CollinearLinear_THM;
    A IN m DELETE O /\ X IN m DELETE O /\ B IN m DELETE O     [AXBm_O] by ABm, Xm, H2', B1_AOB, IN_DELETE; 
    O IN open_int (A,X) by H1, ABm, Om, AXBm_O, K2, IntervalTransitivity_THM;
    O IN open_int (X,A) by -, B1';
  qed by -, IN, Ray_DEF`;;


let OppositeRaysIntersect1point_THM = thm `;
  let A O B be point;
  assume O IN open_int (A,B)                                                       [H1];
  thus ray (O,A) INTER ray (O,B) = {O} 

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B) /\ O IN open_int (B,A) /\ Collinear (A,O,B) [B1_AOB] by H1, B1';
    O IN ray (O,A) INTER ray (O,B) by B1_AOB, OriginInRay_THM, IN_INTER;
    {O} SUBSET ray (O,A) INTER ray (O,B)     [Osubset_rOA] by -, SING_SUBSET; 
    ray (O,A) INTER ray (O,B) SUBSET {O}
    proof
      !X. X IN ray (O,A) INTER ray (O,B) ==> X IN {O}
      proof
        let X be point;
        assume X IN ray (O,A) INTER ray (O,B);
        X IN ray (O,A) /\ X IN ray (O,B)     [XinBothRays] by -, IN_INTER;
        cases;
        suppose X = O;
        qed by -, IN_SING;
        suppose ~(X = O);
          X IN ray (O,B) DELETE O by -, XinBothRays, IN_DELETE;
          ~(X IN ray (O,A)) by H1, -, OppositeRaysIntersect1pointHelp_THM;
          F by -, XinBothRays; 
        qed by -;
      end;
    qed by -, SUBSET;
    qed by -, Osubset_rOA, DoubleSubsetEqual_THM`;;


let TransitivityBetweennessHelp_THM = thm `;
  let A B C D be point;
  assume B IN open_int (A,C) /\ C IN open_int (B,D)     [H1];
  thus B IN open_int (A,D)

  proof
    ~(A  = B) /\ ~(A  = C) /\ ~(B  = C) [Distinct] by H1, B1';
    consider l such that
    Line l /\ A IN l /\ C IN l [ACl] by Distinct, I1;
    B IN l /\ D IN l by ACl, H1, BetweenLinear_THM;
    Collinear (B,A,D) [BADcol] by ACl, -, Collinear_DEF;
    ~(B IN open_int (D,C)) by H1, B1', B3';
    D IN ray (B,C) DELETE B by Distinct, H1, B1', -, IN, Ray_DEF, IN_DELETE;
    ~(D IN ray (B,A)) by Distinct, H1, -, OppositeRaysIntersect1pointHelp_THM; 
    B IN open_int (D,A) by Distinct, BADcol, -, IN, Ray_DEF;
  qed by -, B1'`;;


let TransitivityBetweenness_THM = thm `;
  let A B C D be point;
  assume B IN open_int (A,C) /\ C IN open_int (B,D)     [H1];
  thus is_ordered (A,B,C,D)

  proof
    B IN open_int (A,D)      [ABD] by H1, TransitivityBetweennessHelp_THM;
    C IN open_int (D,B) /\ B IN open_int (C,A)     by H1, B1';
    C IN open_int (D,A)     [DCA] by -, TransitivityBetweennessHelp_THM;
    C IN open_int (A,D)     by -, B1';
  qed by H1, ABD, -, is_ordered_DEF`;;


let IntervalsAreConvex_THM = thm `;
 let A B C be point;
  assume B IN open_int (A,C)     [H1];
  thus open_int (A,B) SUBSET open_int (A,C) 

  proof
    !X. X IN open_int (A,B) ==> X IN open_int (A,C)
    proof
      let X be point;
      assume X IN open_int (A,B)     [XinAB];
     ~(A = X) /\ ~(A = B) /\ ~(A = C) /\ ~(X = B) /\ ~(B = C)     [Distinct] by H1, XinAB, B1';
      consider l such that 
      Line l /\ A IN l /\ C IN l     [ACl] by Distinct, I1;
      B IN l /\ X IN l      by ACl, H1, XinAB, B1', BetweenLinear_THM;
      Collinear (B,C,X)     [BCXcol] by ACl, -, Collinear_DEF;
      Collinear (B,A,X)     [ABXcol] by XinAB, B1', CollinearSymmetry_THM ;
      ~(B IN open_int (X,A))     by Distinct, ABXcol, XinAB, B3';
      X IN ray (B,A) DELETE B     [XrBA_B] by Distinct, ABXcol, -, Ray_DEF, IN, IN_DELETE;
      ~(X IN ray (B,C))     [notXrBC] by H1, B1', XrBA_B, OppositeRaysIntersect1pointHelp_THM;
      B IN open_int (X,C)     by Distinct, BCXcol, notXrBC, IN, Ray_DEF;
      X IN open_int (A,C)     by XinAB, -, TransitivityBetweennessHelp_THM;
    qed by -;
  qed by -, SUBSET`;;


let TransitivityBetweennessVariant_THM = thm `;
  let A X B C be point;
  assume X IN open_int (A,B) /\ B IN open_int (A,C)     [H1];
  thus is_ordered (A,X,B,C)

  proof
    ~(A = X) /\ ~(A = B) /\ ~(A = C) /\ ~(X = B) /\ ~(B = C)     [Distinct] by H1, B1';
    consider l such that 
    Line l /\ A IN l /\ C IN l     [ACl] by Distinct, I1;
    B IN l /\ X IN l     by ACl, H1, B1', BetweenLinear_THM;
    Collinear (B,C,X)     [BCXcol] by H1, ACl, -, Collinear_DEF;
    Collinear (B,A,X)     [ABXcol] by H1, B1', CollinearSymmetry_THM ;
    ~(B IN open_int (X,A))     by Distinct, ABXcol, H1, B3';
    X IN ray (B,A) DELETE B     [XrBA_B] by Distinct, ABXcol, -, Ray_DEF, IN, IN_DELETE;
    ~(X IN ray (B,C))     [notXrBC] by H1, B1', XrBA_B, OppositeRaysIntersect1pointHelp_THM;
    B IN open_int (X,C)     by Distinct, BCXcol, notXrBC, IN, Ray_DEF;
    is_ordered (A,X,B,C)     by H1, -, TransitivityBetweenness_THM;
  qed by -`;;


let Interval2sides2aLineHelp_THM = thm `;
  let A B C X be point;
  let l be point_set;
  assume ~(A = B) /\ ~(A = C) /\ ~(A = X) /\ ~(B = C) /\ ~(B = X) /\ ~(C = X)     [H1];
  assume Line l /\ A IN l /\ B IN l /\ C IN l /\ X IN l     [H2];
  assume B IN open_int (A,C)     [H3];   	       	      
  thus ~(X IN open_int (A,B)) \/ ~(X IN open_int (B,C)) 

  proof
    assume X IN open_int (A,B)     [X_AB];
    Collinear (X,B,C)     [XBCcol] by H2, Collinear_DEF;
    is_ordered (A,X,B,C)     [AXBC] by X_AB, H3, TransitivityBetweennessVariant_THM;
    B IN open_int (X,C)     [B_XC] by AXBC, is_ordered_DEF;
    ~(X IN open_int (C,B)) by H1, XBCcol, B_XC, B3';
  qed by -, B1'`;;


let Interval2sides2aLine_THM = thm `;
  let A B C X be point;
  let l be point_set;
  assume ~(A = B) /\ ~(A = C) /\ ~(A = X) /\ ~(B = C) /\ ~(B = X) /\ ~(C = X)     [H1];
  assume Line l /\ A IN l /\ B IN l /\ C IN l /\ X IN l     [H2];
  thus ~(X IN open_int (A,B)) \/ ~(X IN open_int (B,C)) \/ ~(X IN open_int (A,C))

  proof
    Collinear (A,B,C) by H2, Collinear_DEF;
    B IN open_int (A,C) \/ C IN open_int (B,A) \/ A IN open_int (C,B) by H1, -, B3';
    cases by -;
    suppose B IN open_int (A,C);
    qed by H1, H2, -, Interval2sides2aLineHelp_THM;
    suppose C IN open_int (B,A);
      ~(X IN open_int (B,C)) \/ ~(X IN open_int (C,A)) by H1, H2, -, Interval2sides2aLineHelp_THM; 
    qed by -, B1';
    suppose A IN open_int (C,B);
      ~(X IN open_int (C,A)) \/ ~(X IN open_int (A,B)) by H1, H2, -, Interval2sides2aLineHelp_THM;
    qed by -, B1';
  end`;;


let TwosidesTriangle2aLinePart1_THM = thm `;
  let A B C X Y Z be point;
  let m be point_set;
  assume ~Collinear (A,B,C)			  [H1];
  assume X IN open_int (A,B)           	    	  [H2X];
  assume Z IN open_int (C,B)     		  [H2Z];
  assume Line m /\ A IN m /\ C IN m /\ Y IN m     [m_line];
  assume X IN open_int (Y,Z)     		  [H3];
  thus A IN open_int (Y,C)

  proof
      ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~(Z = B) /\ ~(X = Y) /\ ~(X = Z) [Distinct] by H1, H2X, H2Z, H3, B1', NonCollinearImpliesDistinct_THM;
      consider p such that 
      Line p /\ B IN p /\ A IN p     [p_line] by Distinct, I1;
      consider q such that 
      Line q /\ B IN q /\ C IN q     [q_line] by Distinct, I1;
      consider l such that 
      Line l /\ X IN l /\ Z IN l     [l_line] by Distinct, I1;

      X IN p      	  [Xp] by p_line, H2X, BetweenLinear_THM;
      C IN q DELETE B     [Cq_B] by q_line, Distinct, IN_DELETE;
      Z IN q DELETE B     [Zq_B] by q_line, H2Z, BetweenLinear_THM, Distinct, IN_DELETE;
      Y IN l DELETE X     [Yl_X] by l_line, H3, BetweenLinear_THM, Distinct, IN_DELETE;
       ~(C IN p)           [notCp] by p_line, H1, Collinear_DEF;
     ~(B IN open_int (Z,C))     [notZBC] by H2Z, B1', B3';  
      ~(m = p)            by m_line, notCp;
      m INTER p = {A}     [mpA] by m_line, p_line, -, Line01infinity_THM;
      ~(p = q)     	  by q_line, notCp;
      p INTER q = {B}     [pqB] by p_line, q_line, -, Line01infinity_THM;
      ~(Z IN p)     [notZp] by pqB, Zq_B, EquivIntersectionHelp_THM;
      ~(B IN open_int (C,Z))     by notZBC, B1';  
      C,Z same_side p     [Csim_pZ] by p_line, q_line, pqB, Cq_B, Zq_B, notCp, notZp, -, EquivIntersection_THM;
      ~(Y,Z same_side p)     [Ynsim_pZ] by p_line, Xp, H3, same_side_DEF;
      ~(l = p)     by notZp, l_line;
      p INTER l = {X}     by p_line, l_line, -, Xp, Line01infinity_THM;
      ~(Y IN p)     by -, Yl_X, EquivIntersectionHelp_THM;
      ~(Y,C same_side p)     by p_line, -, notCp, notZp, Csim_pZ, Ynsim_pZ, SameSideTransitiveRelation_THM, Transitive_relation_DEF;
      ~(open_int (Y,C) INTER p = {})     [Ynsim_pC] by -, p_line, same_side_DEF, IN_INTER, MEMBER_NOT_EMPTY;
      open_int (Y,C) SUBSET m     by m_line, m_line, OpenIntervalSubsetLine_THM;
      open_int (Y,C) INTER p SUBSET {A}     by -, SubsetTensor_THM, mpA;
      A IN open_int (Y,C) INTER p     by Ynsim_pC, -, NonemptySubsetSing_THM;
    qed by -, IN_INTER`;;


let TwosidesTriangle2aLinePart2_THM = thm `;
  let A B C X Z be point;
  let m be point_set;
  assume ~Collinear (A,B,C)		[H1];
  assume X IN open_int (A,B)           	[H2X];
  assume Z IN open_int (C,B)     	[H2Z];
  assume Line m /\ A IN m /\ C IN m     [m_line];
  thus ~(X = Z) /\ ~(X IN m) /\ ~(Z IN m) /\ X,Z same_side m

  proof
    ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~(X = A) /\ ~(X = B) /\ ~(Z = C) /\ ~(Z = B) 
    [Distinct] by H1, H2X, H2Z, B1', NonCollinearImpliesDistinct_THM;
    consider p such that 
    Line p /\ B IN p /\ A IN p     [p_line] by Distinct, I1;
    consider q such that 
    Line q /\ B IN q /\ C IN q     [q_line] by Distinct, I1;
    ~(B IN m)     [notBm] by m_line, H1, Collinear_DEF;
    ~(m = p)     by p_line, notBm;
    m INTER p = {A}     [mpA] by m_line, p_line, -, Line01infinity_THM;
    ~(m = q)     by q_line, notBm;
    m INTER q = {C}     [mqC] by q_line, m_line, -, Line01infinity_THM;
    B IN p DELETE A     [Bp_A] by p_line, Distinct, IN_DELETE;
    B IN q DELETE C     [Bq_C] by q_line, Distinct, IN_DELETE;
    X IN p /\ X IN p DELETE A /\ X IN p DELETE B     [Xp] by p_line, H2X, BetweenLinear_THM, Distinct, IN_DELETE;
    Z IN q /\ Z IN q DELETE C /\ Z IN q DELETE B     [Zq] by q_line, H2Z, BetweenLinear_THM, Distinct, IN_DELETE;
    ~(A IN q)     by q_line, H1, Collinear_DEF;
    ~(p = q)     by p_line, -;
    p INTER q = {B}     by p_line, q_line, -, Line01infinity_THM;
    ~(Z IN p)     by -, Zq, EquivIntersectionHelp_THM;
    ~(X = Z)      [notXZ] by Xp, -;
    ~(X IN m)     [notXm] by mpA, Xp, EquivIntersectionHelp_THM;
    ~(Z IN m)     [notZm] by mqC, Zq, EquivIntersectionHelp_THM;
    ~(A IN open_int (X,B))     by Distinct, B1', H2X, B3';
    X,B same_side m     [Xsim_mB] by m_line, p_line, mpA, Xp, Bp_A, -, EquivIntersection_THM;
    ~(C IN open_int (B,Z))     by Distinct, B1', H2Z, B3';
    B,Z same_side m     by m_line, q_line, mqC, Zq, Bq_C, -, EquivIntersection_THM;
    X,Z same_side m     by m_line, notXm, notBm, notZm, Xsim_mB, -, SameSideTransitiveRelation_THM, Transitive_relation_DEF;
  qed by notXZ, notXm, notZm, -`;;


let TwosidesTriangle2aLine_THM = thm `;
  let A B C be point;
  let l be point_set;
  assume Line l /\ ~Collinear (A,B,C)			[H1];
  assume ~(A IN l) /\ ~(B IN l) /\ ~(C IN l)      	[off_l];
  thus A,B same_side l \/ B,C same_side l \/ A,C same_side l

  proof
    (A,B same_side l \/ B,C same_side l) \/ A,C same_side l
    proof
      assume ~(A,B same_side l \/ B,C same_side l);
      ~(A,B same_side l) /\ ~(B,C same_side l) [H2] by -;
      consider X such that
      X IN l /\ X IN open_int (A,B)     [H2X]  by H1, H2, same_side_DEF;
      consider Z such that
      Z IN l /\ Z IN open_int (B,C)     [H2Z]  by H1, H2, same_side_DEF;
      ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~(X = A) /\ ~(X = B) /\ ~(Z = C) /\ ~(Z = B) 
      [Distinct] by H1, H2X, H2Z, B1', NonCollinearImpliesDistinct_THM;
      consider p such that 
      Line p /\ B IN p /\ A IN p     [p_line] by Distinct, I1;
      consider q such that 
      Line q /\ B IN q /\ C IN q     [q_line] by Distinct, I1;
      consider m such that 
      Line m /\ A IN m /\ C IN m     [m_line] by Distinct, I1;
      Z IN open_int (C,B)     [H2Z'] by H2Z, B1';
      ~(X = Z) /\ ~(X IN m) /\ ~(Z IN m) /\ X,Z same_side m     [Xsim_mZ]  by H1, H2X, H2Z', m_line, TwosidesTriangle2aLinePart2_THM;
      cases;
      suppose l INTER m = {} [lmDisjoint];
	open_int (A,C) SUBSET m     by m_line, OpenIntervalSubsetLine_THM;
	l INTER open_int (A,C) = {}     by -, SubsetTensor_THM, lmDisjoint, SUBSET_EMPTY;
      qed by H1, -, IN_INTER, NOT_IN_EMPTY, same_side_DEF;
      suppose ~(l INTER m = {});
	consider Y such that 
	Y IN l /\ Y IN m     [Ylm] by -, MEMBER_NOT_EMPTY, IN_INTER;
	 ~(l = m)     by H2X, Xsim_mZ;
	l INTER m = {Y}     [lmY] by H1, m_line, -, Ylm, Line01infinity_THM;
       	~(Y IN open_int (X,Z))     [notXYZ] by H1, Ylm, Xsim_mZ, same_side_DEF;
	Collinear (X,Y,Z) [XYZcol]     by H1, H2X, Ylm, H2Z, Collinear_DEF;
	~(X = Y) /\ ~(X = Z) /\ ~(Y = Z)     [distinctXYZ] by Ylm, Xsim_mZ;
	~(Y = A) /\ ~(Y = C)     by Ylm, off_l;
	A IN m DELETE Y /\ C IN m DELETE Y     [ACm_Y] by m_line, -, IN_DELETE;
	Z IN open_int (Y,X) \/ X IN open_int (Z,Y)     by distinctXYZ, XYZcol, notXYZ, B3';
	cases by -;
	suppose X IN open_int (Z,Y) [ZXY];
	  A IN open_int (Y,C)     by H1, H2X, H2Z, B1', Ylm, m_line, ZXY, TwosidesTriangle2aLinePart1_THM;
	  ~(Y IN open_int (C,A))     by -, B1', B3';
	  ~(Y IN open_int (A,C))     [notAYC] by -, B1';
	qed by H1, m_line, lmY, ACm_Y, notAYC, EquivIntersection_THM;
	suppose Z IN open_int (Y,X) [YZX];
	  ~Collinear (C,B,A) /\ Z IN open_int (C,B) by H1, CollinearSymmetry_THM, H2Z, B1';
	  C IN open_int (Y,A)     by -, H2X, Ylm, m_line, YZX, TwosidesTriangle2aLinePart1_THM;
	  ~(Y IN open_int (A,C))     by -, B1', B3';
	qed by H1, m_line, lmY, ACm_Y, -, EquivIntersection_THM;
      end;
    end;
  qed by -`;;   


let LineUnionOf2Rays_THM = thm `;
  let A O B be point;
  let l be point_set;
  assume Line l /\ A IN l /\ B IN l     [H1];
  assume O IN open_int (A,B)                   [H2];
  thus l = ray (O,A) UNION ray (O,B)

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H2, B1';
    O IN l [Ol] by H1, H2, BetweenLinear_THM;
    ray (O,A) SUBSET l /\ ray (O,B) SUBSET l by H1, -, RayLine_THM;
    ray (O,A) UNION ray (O,B) SUBSET l [AOBsub_l] by -, UNION_SUBSET;
    !X. X IN l ==> X IN ray (O,A) \/ X IN ray (O,B) 
    proof
      let X be point;
      assume X IN l [Xl];
      assume ~(X IN ray (O,B)) [notXrOB];
      Collinear (O,A,X) [OAXcol] by Ol, H1, Xl, Collinear_DEF;
      cases;
      suppose X = A;
      qed by -, Distinct, EndpointInRay_THM;
      suppose ~(X = A) [notXA];
        Collinear (O,B,X) by Ol, H1, Xl, Collinear_DEF;
      	O IN open_int (X,B) [XOB] by notXrOB, Distinct, -, IN, Ray_DEF;     
      	~(X = O) /\ ~(X = B) by -, B1';
        ~(O IN open_int (X,A)) by Distinct, -, notXA, H1, Ol, Xl, H2, XOB, Interval2sides2aLine_THM;
      qed by Distinct, OAXcol, -, IN, Ray_DEF;
    end;
    !X. X IN l ==> X IN ray (O,A) UNION ray (O,B) by -, IN_UNION;
    l SUBSET ray (O,A) UNION ray (O,B) by -, SUBSET;
  qed by -, AOBsub_l, SUBSET_ANTISYM`;;


let AtMost2Sides_THM = thm `;
  let A B C be point;
  let l be point_set;
  assume Line l							[H1];
  assume ~(A IN l) /\ ~(B IN l) /\ ~(C IN l)    		[H2];
  thus A,B same_side l \/ A,C same_side l \/ B,C same_side l

  proof
    cases;
    suppose ~Collinear (A,B,C);
    qed by H1, -, H2, TwosidesTriangle2aLine_THM;
    suppose Collinear (A,B,C)     [ABCcol];
      cases by -;
      suppose A = B \/ A = C \/ B = C;
      qed by -, H1, H2, SameSideReflexiveRelation_THM, Reflexive_relation_DEF;
      suppose ~(A = B) /\ ~(A = C) /\ ~(B = C)     [Distinct];
        consider m such that 
        Line m /\ A IN m /\ B IN m     [m_line] by Distinct, I1;
        C IN m     [Cm] by m_line, ABCcol, Distinct, CollinearLinear_THM;
        cases;
        suppose l INTER m = {}     [lmDisjoint];
          open_int (A,B) SUBSET m      by m_line, OpenIntervalSubsetLine_THM;
          l INTER open_int (A,B) = {}     by -, SubsetTensor_THM, lmDisjoint, SUBSET_EMPTY;
          A,B same_side l     by H1, -, IN_INTER, NOT_IN_EMPTY, same_side_DEF;
        qed by -;
        suppose ~(l INTER m = {});
          consider X such that 
          X IN l /\ X IN m     [Xlm] by -, IN_INTER, MEMBER_NOT_EMPTY;
          ~(A = X) /\ ~(B = X) /\ ~(C = X)     [ABCnotX] by Xlm, H2;
          A IN m DELETE X /\ B IN m DELETE X /\ C IN m DELETE X     [ABCm_X] by m_line, Cm, ABCnotX, IN_DELETE;
          ~(l = m)      by H2, m_line;
          l INTER m = {X} [lmX]     by H1, m_line, -, Xlm, Line01infinity_THM;
          ~(X IN open_int (A,B)) \/ ~(X IN open_int (A,C)) \/ ~(X IN open_int (B,C))     by Distinct, ABCnotX, m_line, Cm, Xlm, Interval2sides2aLine_THM;
        qed by H1, m_line, lmX, ABCm_X, -, EquivIntersection_THM;
      end;
    end;
  end`;;
   

let FourPointsOrder1_THM = thm `;
  let A B C X be point;
  let l be point_set;
  assume Line l /\ A IN l /\ B IN l /\ C IN l /\ X IN l		[H1];
  assume ~(A  =  B) /\ ~(A  =  C) /\ ~(A  =  X) /\ 
  	 ~(B  =  C) /\ ~(B  =  X) /\ ~(C  =  X)			[H2];
  assume B IN open_int (A,C)         	     			[H3];
  thus A IN open_int (X,B) \/ X IN open_int (A,B) \/ 
       X IN open_int (B,C) \/ C IN open_int (B,X)

  proof
   Collinear (A,B,X) /\ Collinear (C,B,X)     [ABCXcol] by H1, Collinear_DEF;
   A IN open_int (X,B) \/ X IN open_int (A,B) \/ B IN open_int (A,X)     by H2, ABCXcol, B3', B1';
   cases by -;
   suppose A IN open_int (X,B) \/ X IN open_int (A,B);
   qed by -;
   suppose B IN open_int (A,X);
     ~(B IN open_int (C,X))     by H2, H1, H3, -, Interval2sides2aLine_THM;
     X IN open_int (B,C) \/ C IN open_int (B,X)     by H2, ABCXcol, -, B3', B1'; 
   qed by -;
  end`;;


let FourPointsOrder_THM = thm `;
  let A B C X be point;
  let l be point_set;
  assume Line l /\ A IN l /\ B IN l /\ C IN l /\ X IN l		[H1];
  assume ~(A = B) /\ ~(A = C) /\ ~(A = X) /\ 
  	 ~(B = C) /\ ~(B = X) /\ ~(C = X)			[H2];
  assume B IN open_int (A,C)         	     			[H3];
  thus is_ordered (X,A,B,C) \/ is_ordered (A,X,B,C) \/ 
       is_ordered (A,B,X,C) \/ is_ordered (A,B,C,X)

  proof
    A IN open_int (X,B) \/ X IN open_int (A,B) \/ 
    X IN open_int (B,C) \/ C IN open_int (B,X)     by H1, H2, H3, FourPointsOrder1_THM;  
    cases by -;
    suppose A IN open_int (X,B);
      is_ordered (X,A,B,C)     by -, H3, TransitivityBetweenness_THM;
    qed by -;
    suppose X IN open_int (A,B);
      is_ordered (A,X,B,C)     by -, H3, TransitivityBetweennessVariant_THM;
    qed by -;
    suppose X IN open_int (B,C);
      X IN open_int (C,B) /\ B IN open_int (C,A)     by -, H3, B1';
      is_ordered (C,X,B,A) by -, TransitivityBetweennessVariant_THM;
    qed     by -, Reverse4Order_THM;
    suppose C IN open_int (B,X);
      is_ordered (A,B,C,X) by H3, -, TransitivityBetweenness_THM;
    qed by -;
  end`;;


let HilbertAxiomRedundantByMoore_THM = thm `;
  let A B C D be point;
  let l be point_set;
  assume Line l /\ A IN l /\ B IN l /\ C IN l /\ D IN l		[H1];
  assume ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ 
  	 ~(B = C) /\ ~(B = D) /\ ~(C = D)			[H2];
  thus is_ordered (D,A,B,C) \/ is_ordered (A,D,B,C) \/ is_ordered (A,B,D,C) \/ is_ordered (A,B,C,D) \/
       is_ordered (D,A,C,B) \/ is_ordered (A,D,C,B) \/ is_ordered (A,C,D,B) \/ is_ordered (A,C,B,D) \/
       is_ordered (D,C,A,B) \/ is_ordered (C,D,A,B) \/ is_ordered (C,A,D,B) \/ is_ordered (C,A,B,D)

  proof
    Collinear (A,B,C) by H1, Collinear_DEF;
    B IN open_int (A,C) \/ C IN open_int (A,B) \/ A IN open_int (C,B) by H2, -, B3', B1';
  qed by -, H1, H2, FourPointsOrder_THM`;;


let InteriorWellDefined_THM = thm `;
  let A O B X P be point;
  assume P int_angle A,O,B [H1];
  assume X IN ray (O,B) DELETE O [H2];
  thus P int_angle A,O,X

  proof
    consider a b such that
    ~Collinear (A,O,B) /\ Line a /\ O IN a /\ A IN a /\ ~(P IN a) /\ 
    Line b /\ O IN b /\ B IN b /\ ~(P IN b) /\ 
    P,B same_side a /\ P,A same_side b     [def_int] by H1, InteriorAngle_DEF;
    X IN ray (O,B) /\ ~(X = O) [H2']     by H2, IN_DELETE;
    ~(A = O) /\ ~(A = B) /\ ~(O = B)     [AOBdistinct] by def_int, NonCollinearImpliesDistinct_THM;
    ~(A IN b)     by def_int, Collinear_DEF;
    ~(a = b)     by -, def_int;
    a INTER b = {O}     [abO] by def_int, -, Line01infinity_THM;
    ~(O = B) /\ Collinear (O,B,X) /\ ~(O IN open_int (X,B))     [XrOB_O] by H2', IN, Ray_DEF;
    X IN b  [Xb]     by def_int, XrOB_O, CollinearLinear_THM, H2';
    X IN b DELETE O     [Xb_O] by -, H2', IN_DELETE;
    ~(B IN a)     [notBa] by def_int, Collinear_DEF;
    ~(X IN a)     [notXa] by abO, Xb_O, EquivIntersectionHelp_THM;
    ~Collinear (A,O,X) [AOXnoncol]     by def_int, AOBdistinct, notXa, CollinearLinear_THM;
    B IN b DELETE O     by def_int, abO, AOBdistinct, IN_DELETE;
    B,X same_side a     by def_int, abO, -, Xb_O, XrOB_O, B1', notBa, notXa, EquivIntersection_THM;
    P,X same_side a     by def_int, notXa, notBa, -, SameSideTransitiveRelation_THM, Transitive_relation_DEF;
  qed by AOXnoncol, def_int, Xb, -, InteriorAngle_DEF`;;


let InteriorTransitivity_THM = thm `;
  let A O B F G be point;
  assume ~Collinear (A,O,B) [H1];
  assume G int_angle A,O,B [H2];
  assume F int_angle A,O,G [H3];
  thus F int_angle A,O,B

  proof
    ~(A = O) /\ ~(A = B) /\ ~(O = B)     [Distinct] by H1, NonCollinearImpliesDistinct_THM;
    ~(G = A) /\ ~(G = O) /\ ~(G = B) /\ ~Collinear (A,O,G)     [GnotAOB] by H2, InteriorEZHelp_THM;
    consider G0 such that 
    G0 IN open_int (A,B) /\ G0 IN ray (O,G) DELETE O     [CrossG] by H1, H2, Crossbar_THM;
    G0 int_angle A,O,B     by H1, H2, CrossG, IN_DELETE, WholeRayInterior_THM;
    ~(G0 = O)     by -, InteriorEZHelp_THM;
    F int_angle A,O,G0     [F_AOG0] by H3, CrossG, InteriorWellDefined_THM;
    ~Collinear (A,O,G0)     by F_AOG0, InteriorAngle_DEF;
    consider F0 such that
    F0 IN open_int (A,G0) /\ F0 IN ray (O,F) DELETE O     [CrossF] by -, F_AOG0, Crossbar_THM;
    ~(F = O)     [notFO] by H3, InteriorEZHelp_THM;
    open_int (A,G0) SUBSET open_int (A,B)     by CrossG, IntervalsAreConvex_THM;
    F0 IN open_int (A,B)     by CrossF, -, SUBSET;
    F0 int_angle A,O,B [F0_A0B]     by H1, -, ConverseCrossbar_THM;
    ray (O,F0) = ray (O,F)     by notFO, CrossF, RayWellDefined_THM;
    F IN ray (O,F0)     by -, notFO, EndpointInRay_THM;
  qed by H1, F0_A0B, -, notFO, WholeRayInterior_THM`;;


let Tetralateral_DEF = new_definition
  `Tetralateral (A,B,C,D)  <=> 
  ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) /\ 
  ~Collinear (A,B,C) /\ ~Collinear (B,C,D) /\ ~Collinear (C,D,A) /\ ~Collinear (D,A,B)`;;


let TetralateralSymmetry_THM = thm `;
  let A B C D be point;
  assume Tetralateral (A,B,C,D)			[H1];
  thus Tetralateral (B,C,D,A)

  proof
        ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) /\ 
  	~Collinear (A,B,C) /\ ~Collinear (B,C,D) /\ ~Collinear (C,D,A) /\ ~Collinear (D,A,B) by H1, Tetralateral_DEF;
  qed by -, Tetralateral_DEF`;;


let EasyEmptyIntersectionsTetralateralHelp_THM = thm `;
  let A B C D be point;
  assume Tetralateral (A,B,C,D)			[H1];
  thus open_int (A,B) INTER open_int (B,C) = {}

  proof
    ~(A = B) /\ ~(B = C) /\ ~(C = D) /\ ~(D = A) /\ 
    ~Collinear (A,B,C)     [noncolDistinct] by H1, Tetralateral_DEF;
    consider a such that Line a /\ A IN a /\ B IN a [a_line] by noncolDistinct, I1;
    consider b such that Line b /\ B IN b /\ C IN b [b_line] by noncolDistinct, I1;
    consider c  such that Line c /\ C IN c /\ D IN c [c_line] by noncolDistinct, I1;
    consider d such that Line d /\ D IN d /\ A IN d [d_line] by noncolDistinct, I1;
    ~(C IN a)     by a_line, noncolDistinct, Collinear_DEF;
    ~(a = b)     by -, a_line, b_line;
    a INTER b = {B} [abB]     by a_line, b_line, -, Line01infinity_THM;
    open_int (A,B) SUBSET a /\ open_int (B,C) SUBSET b     by a_line, b_line, OpenIntervalSubsetLine_THM;
    open_int (A,B) INTER open_int (B,C) SUBSET {B}     [AB_BC_B] by -, SubsetTensor_THM, INTER_COMM, SUBSET_TRANS, abB;
    ~(B IN open_int (A,B))     by B1';
    ~(B IN open_int (A,B) INTER open_int (B,C))     by -, IN_INTER;
    open_int (A,B) INTER open_int (B,C) = {}     by -, AB_BC_B, MEMBER_NOT_EMPTY, IN_SING, SUBSET;
  qed by -`;;


let EasyEmptyIntersectionsTetralateral_THM = thm `;
  let A B C D be point;
  assume Tetralateral (A,B,C,D)                       [H1];
  thus open_int (A,B) INTER open_int (B,C) = {} /\ 
       open_int (B,C) INTER open_int (C,D) = {} /\ 
       open_int (C,D) INTER open_int (D,A)  = {} /\ 
       open_int (D,A) INTER open_int (A,B)  = {}

  proof
    open_int (A,B) INTER open_int (B,C) = {} [B] by H1, EasyEmptyIntersectionsTetralateralHelp_THM;
    Tetralateral (B,C,D,A) [BCDA] by H1, TetralateralSymmetry_THM;
    open_int (B,C) INTER open_int (C,D) = {} [C] by -, EasyEmptyIntersectionsTetralateralHelp_THM;
    Tetralateral (C,D,A,B) [CDAB] by BCDA, TetralateralSymmetry_THM;
    open_int (C,D) INTER open_int (D,A)  = {} [D] by -, EasyEmptyIntersectionsTetralateralHelp_THM;
    Tetralateral (D,A,B,C) [DABC] by CDAB, TetralateralSymmetry_THM;
  qed by B, C, D, -, EasyEmptyIntersectionsTetralateralHelp_THM`;;


let Quadrilateral_DEF = new_definition
  `Quadrilateral (A,B,C,D)  <=> 
  Tetralateral (A,B,C,D) /\ 
  open_int (A,B) INTER open_int (C,D) = {} /\ 
  open_int (B,C) INTER open_int (D,A) = {} `;;

let ConvexQuad_DEF = new_definition
  `ConvexQuadrilateral (A,B,C,D)  <=> 
  Quadrilateral (A,B,C,D) /\ 
  A int_angle B,C,D /\ B int_angle C,D,A /\ C int_angle D,A,B /\  D int_angle A,B,C `;;


let SegmentSameSideOppositeLine_THM = thm `;
  let A B C D be point;
  let a c be point_set;
  assume Quadrilateral (A,B,C,D) [H1];
  assume Line a /\ A IN a /\ B IN a [a_line];
  assume Line c /\ C IN c /\ D IN c [c_line];
  thus A,B same_side c \/ C,D same_side a

  proof
    assume ~(C,D same_side a)     [Cnsim_aD];
    Tetralateral (A,B,C,D) /\
    open_int (A,B) INTER open_int (C,D) = {}     [quadABCD] by H1, Quadrilateral_DEF;
    ~Collinear (B,C,D) /\ ~Collinear (C,D,A)     by quadABCD, Tetralateral_DEF;
      ~(A IN c) /\ ~(B IN c)     [notABc] by -, c_line, Collinear_DEF;
   consider G such that 
    G IN a /\ G IN open_int (C,D)     [GaCD] by Cnsim_aD, a_line, same_side_DEF;
    open_int (C,D) SUBSET c     by c_line, OpenIntervalSubsetLine_THM;
    G IN c     [Gc] by GaCD, -, SUBSET;
     ~(a = c) by notABc, a_line;
    c INTER a = {G}     [caG] by a_line, c_line,  -,  GaCD, Gc, Line01infinity_THM;
    ~(G IN open_int (A,B))     [notAGB] by quadABCD, GaCD, DisjointOneNotOther_THM;
    ~(A = G) /\ ~(B = G)     by notABc, Gc;
    A IN a DELETE G /\ B IN a DELETE G     by a_line, -, IN_DELETE;
    A,B same_side c by a_line, c_line, caG, -, notAGB, EquivIntersection_THM;

  qed by -`;;