(* ----------------------------------------------------------------- *)
(* HOL Light Hilbert geometry axiomatic proofs using miz3.           *)
(* ----------------------------------------------------------------- *)

(* High school students can learn rigorous axiomatic Geometry proofs,
   as in http://www.math.northwestern.edu/~richter/hilbert.pdf, using
   Hilbert's axioms, and code up their proofs in miz3 and HOL Light.
   Thanks to Bjørn Jahren, Miguel Lerma,Takuo Matsuoka, Stephen
   Wilson for advice on Hilbert's axioms, and especially Benjamin
   Kordesh, who carefully read much of the paper and the code.

   Formal proofs are given for the first 7 sections of the paper, the
   results cited there from Greenberg's book, and most of Euclid's
   book I propositions up to Proposition I.29, following Hartshorne,
   whose book seems the most exciting axiomatic geometry text.  A
   proof assistant is an valuable tool to help read it, as
   Hartshorne's proofs are often sketchy and even have gaps.

   M. Greenberg, Euclidean and non-Euclidean geometries, W. H. Freeman and Co., 1974.
   R. Hartshorne, Geometry, Euclid and Beyond, Undergraduate Texts in Math., Springer, 2000.

   Thanks to Mizar folks for their influential language, Freek
   Wiedijk, who wrote the miz3 port of Mizar to HOL Light, and
   especially John Harrison, who was extremely helpful and developed
   the framework for porting my axiomatic proofs to HOL Light.  *)

verbose := false;;
report_timing := false;;

horizon := 0;;
timeout := 50;;

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

parse_as_infix("≅",(12, "right"));;
parse_as_infix("same_side",(12, "right"));;
parse_as_infix("≡",(12, "right"));;
parse_as_infix("<__",(12, "right"));;
parse_as_infix("<_ang",(12, "right"));;
parse_as_infix("suppl",(12, "right"));;
parse_as_infix("∉",(11, "right"));;
parse_as_infix("∥",(12, "right"));;

let ∉ = new_definition
  `∀a:A l:A->bool. a ∉ l ⇔ ¬(a ∈ l)`;;
let Interval_DEF = new_definition
  `∀ A B. open (A,B) = {X | Between A X B}`;;
let Collinear_DEF = new_definition
  `Collinear A B C  ⇔
  ∃ l. Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l`;;
let SameSide_DEF = new_definition
  `A,B same_side l  ⇔
  Line l ∧ ¬ ∃ X. (X ∈ l) ∧  X ∈ open (A,B)`;;
let Ray_DEF = new_definition
  `∀ A B. ray A B = {X | ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)}`;;
let Ordered_DEF = new_definition
 `ordered A B C D  ⇔
  B ∈ open (A,C) ∧ B ∈ open (A,D) ∧ C ∈ open (A,D) ∧ C ∈ open (B,D)`;;
let InteriorAngle_DEF = new_definition
 `∀ A O B.  int_angle A O B =
    {P:point | ¬Collinear A O B ∧ ∃ a b.
               Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
               P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b}`;;
let InteriorTriangle_DEF = new_definition
 `∀ A B C.  int_triangle A B C =
    {P | P ∈ int_angle A B C  ∧
         P ∈ int_angle B C A  ∧
         P ∈ int_angle C A B}`;;
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 Quadrilateral_DEF = new_definition
  `Quadrilateral A B C D  ⇔
  Tetralateral A B C D ∧
  open (A,B) ∩ open (C,D) = ∅ ∧
  open (B,C) ∩ open (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 Segment_DEF = new_definition
  `seg A B = {A, B} UNION open (A,B)`;;
let SEGMENT = new_definition
  `Segment s  ⇔  ∃ A B. s = seg A B ∧ ¬(A = B)`;;
let SegmentOrdering_DEF = new_definition
 `s <__ t   ⇔
  Segment s ∧
  ∃ C D X. t = seg C D ∧ X ∈ open (C,D) ∧ s ≡ seg C X`;;
let Angle_DEF = new_definition
 ` ∡ A O B = ray O A UNION ray O B `;;
let ANGLE = new_definition
 `Angle α  ⇔  ∃ A O B. α = ∡ A O B ∧ ¬Collinear A O B`;;
let AngleOrdering_DEF = new_definition
 `α <_ang β  ⇔
  Angle α ∧
  ∃ A O B G. ¬Collinear A O B  ∧  β = ∡ A O B ∧
             G ∈ int_angle A O B  ∧  α ≡ ∡ A O G`;;
let RAY = new_definition
 `Ray r  ⇔  ∃ O A. ¬(O = A) ∧ r = ray O A`;;
let TriangleCong_DEF = new_definition
 `∀ A B C A' B' C' :point. (A, B, C) ≅ (A', B', C')  ⇔
  ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
  seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧ seg B C ≡ seg B' C' ∧
  ∡ A B C ≡ ∡ A' B' C' ∧
  ∡ B C A ≡ ∡ B' C' A' ∧
  ∡ C A B ≡ ∡ C' A' B'`;;
let SupplementaryAngles_DEF = new_definition
 `∀ α β. α suppl β   ⇔
  ∃ A O B A'. ¬Collinear A O B  ∧  O ∈ open (A,A')  ∧  α = ∡ A O B  ∧  β = ∡ B O A'`;;
let RightAngle_DEF = new_definition
 `∀ α. Right α  ⇔  ∃ β. α suppl β ∧ α ≡ β`;;
let PlaneComplement_DEF = new_definition
 `∀ α:point_set. complement α = {P | P ∉ α}`;;
let CONVEX = new_definition
 `Convex α  ⇔  ∀ A B. A ∈ α ∧ B ∈ α  ⇒ open (A,B) ⊂ α`;;
let PARALLEL = new_definition
 `∀ l k. l ∥ k   ⇔
  Line l ∧ Line k ∧ l ∩ k = ∅`;;
let Parallelogram_DEF = new_definition
  `∀ A B C D. Parallelogram A B C D  ⇔
  Quadrilateral A B C D ∧ ∃ a b c d.
  Line a ∧ A ∈ a ∧ B ∈ a ∧
  Line b ∧ B ∈ b ∧ C ∈ b ∧
  Line c  ∧ C ∈ c ∧ D ∈ d ∧
  Line d ∧ D ∈ d ∧ A ∈ d ∧
  a ∥ c  ∧  b ∥ d`;;
let InteriorCircle_DEF = new_definition
 `∀ O R.  int_circle O R = {P | ¬(O = R) ∧ (P = O  ∨  seg O P <__ seg O R)}
`;;

(* ----------------------------------------------------------------------------  *)
(* Hilbert's geometry axioms, except the parallel axiom P, defined near the end. *)
(* ----------------------------------------------------------------------------  *)


let I1 = new_axiom
  `∀ A B.  ¬(A = B) ⇒ ∃! l. Line l ∧  A ∈ l ∧ B ∈ l`;;

let I2 = new_axiom
  `∀ l. Line l  ⇒  ∃ A B. A ∈ l ∧ B ∈ 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 ∉ l ∧ B ∉ l ∧ C ∉ l ∧
   (∃ X. X ∈ l ∧ Between A X C) ⇒
   (∃ Y. Y ∈ l ∧ Between A Y B) ∨ (∃ Y. Y ∈ l ∧ Between B Y C)`;;

let C1 = new_axiom
  `∀ s O Z. Segment s ∧ ¬(O = Z)  ⇒
   ∃! P. P ∈ ray O Z ━ O  ∧  seg O P ≡ s`;;

let C2Reflexive = new_axiom
  `Segment s  ⇒  s ≡ s`;;

let C2Symmetric = new_axiom
  `Segment s ∧ Segment t ∧ s ≡ t  ⇒  t ≡ s`;;

let C2Transitive = new_axiom
  `Segment s ∧ Segment t ∧ Segment u ∧
   s ≡ t ∧ t ≡ u ⇒  s ≡ u`;;

let C3 = new_axiom
  `∀ A B C A' B' C'.  B ∈ open (A,C) ∧ B' ∈ open (A',C') ∧
  seg A B ≡ seg A' B' ∧ seg B C ≡ seg B' C'  ⇒
  seg A C ≡ seg A' C'`;;

let C4 = new_axiom
 `∀ α O A l Y. Angle α ∧ ¬(O = A) ∧ Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l
    ⇒ ∃! r. Ray r  ∧  ∃ B. ¬(O = B)  ∧  r = ray O B  ∧
          B ∉ l  ∧  B,Y same_side l  ∧  ∡ A O B ≡ α`;;

let C5Reflexive = new_axiom
  `Angle α  ⇒  α ≡ α`;;

let C5Symmetric = new_axiom
  `Angle α ∧ Angle β ∧ α ≡ β  ⇒  β ≡ α`;;

let C5Transitive = new_axiom
  `Angle α ∧ Angle β ∧ Angle γ ∧
   α ≡ β ∧ β ≡ γ ⇒  α ≡ γ`;;

let C6 = new_axiom
  `∀ A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
   seg B A ≡ seg B' A' ∧ seg B C ≡ seg B' C' ∧ ∡ A B C ≡ ∡ A' B' C'
   ⇒ ∡ B C A ≡ ∡ B' C' A'`;;


(* ----------------------------------------------------------------- *)
(* Theorems.                                                         *)
(* ----------------------------------------------------------------- *)


let IN_Interval = thm `;
 ∀ A B X. X ∈ open (A,B)  ⇔  Between A X B
 by Interval_DEF, SET_RULE;
`;;

let IN_Ray = thm `;
 ∀ A B X. X ∈ ray A B  ⇔  ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)
 by Ray_DEF, SET_RULE;
`;;

let IN_InteriorAngle = thm `;
 ∀ A O B P. P ∈ int_angle A O B  ⇔
     ¬Collinear A O B ∧ ∃ a b.
     Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
     P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b
 by InteriorAngle_DEF, SET_RULE;
`;;

let IN_InteriorTriangle = thm `;
 ∀ A B C P. P ∈ int_triangle A B C  ⇔
     P ∈ int_angle A B C  ∧  P ∈ int_angle B C A  ∧  P ∈ int_angle C A B
 by InteriorTriangle_DEF, SET_RULE;
`;;

let IN_PlaneComplement = thm `;
  ∀ α:point_set. ∀ P. P ∈ complement α  ⇔  P ∉ α
  by PlaneComplement_DEF, SET_RULE;
`;;

let IN_InteriorCircle = thm `;
 ∀ O R P. P ∈ int_circle O R  ⇔
     ¬(O = R) ∧ (P = O  ∨  seg O P <__ seg O R)
 by InteriorCircle_DEF, SET_RULE;
`;;

let B1' = thm `;
  ∀ A B C.  B ∈ open (A,C) ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
             B ∈ open (C,A) ∧ Collinear A B C
  by IN_Interval, B1;
`;;

let B2' = thm `;
  ∀ A B. ¬(A = B) ⇒ ∃ C.  B ∈ open (A,C)
  by IN_Interval, B2;
`;;

let B3' = thm `;
  ∀ A B C. ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
    ⇒ (B ∈ open (A,C) ∨ C ∈ open (B,A) ∨ A ∈ open (C,B)) ∧
        ¬(B ∈ open (A,C) ∧ C ∈ open (B,A)) ∧
        ¬(B ∈ open (A,C) ∧ A ∈ open (C,B)) ∧
        ¬(C ∈ open (B,A) ∧ A ∈ open (C,B))
  by IN_Interval, B3;
`;;

let B4' = thm `;
  ∀ l A B C. Line l ∧ ¬Collinear A B C ∧
   A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
   (∃ X. X ∈ l ∧  X ∈ open (A,C)) ⇒
   (∃ Y. Y ∈ l ∧  Y ∈ open (A,B)) ∨ (∃ Y. Y ∈ l ∧  Y ∈ open (B,C))
   by IN_Interval, B4;
`;;

let B4'' = thm `;
  ∀ l:point_set. ∀ A B C:point.
  Line l ∧ ¬Collinear A B C ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l  ∧
  A,B same_side l  ∧  B,C same_side l  ⇒  A,C same_side l
  by B4', SameSide_DEF;
`;;

let DisjointOneNotOther = thm `;
  ∀ l m:A->bool. (∀ x:A. x ∈ m  ⇒ x ∉ l)  ⇔  l ∩ m = ∅
  by SET_RULE, ∉;
`;;

let EquivIntersectionHelp = thm `;
  ∀ e x:A. ∀ l m:A->bool.
  (l ∩ m = {x}  ∨  m ∩ l = {x})  ∧  e ∈ m ━ x   ⇒  e ∉ l
  by SET_RULE, ∉;
`;;

let CollinearSymmetry = 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 ∈ l ∧ B ∈ l ∧ C ∈ l     by H1, Collinear_DEF;
  qed     by -, Collinear_DEF;
`;;

let ExistsNewPointOnLine = thm `;
  let P be point;
  let l be point_set;
  assume Line l ∧ P ∈ l [H1];
  thus ∃ Q. Q ∈ l ∧ ¬(P = Q)

  proof
    consider A B such that
    A ∈ l ∧ B ∈ l ∧ ¬(A = B)    [l_line] by H1, I2;
    cases;
    suppose P = A;
    qed by -, l_line;
    suppose ¬(P = A);
    qed by -, l_line;
  end;
`;;

let ExistsPointOffLine = thm `;
  let l be point_set;
  assume Line l     [H1];
  thus ∃ Q:point. Q ∉ l

  proof
    consider A B C such that
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear A B C     [Distinct] by I3;
    (A ∉ l ∨ B ∉ l ∨ C ∉ l) ∨ (A ∈ l ∧ B ∈ l ∧ C ∈ l) by ∉;
    cases by -;
    suppose A ∉ l ∨ B ∉ l ∨ C ∉ l;
    qed     by -;
    suppose (A ∈ l) ∧ (B ∈ l) ∧ (C ∈ l);
      Collinear A B C     by H1, -, Collinear_DEF;
    qed     by -, Distinct;
  end;
`;;

let BetweenLinear = thm `;
  let A B C be point;
  let m be point_set;
  assume Line m ∧ A ∈ m ∧ C ∈ m     [H1];
  assume B ∈ open (A,C) ∨ C ∈ open (B,A)  ∨ A ∈ open (C,B)     [H2];
  thus B ∈ 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 ∈ l ∧ B ∈ l ∧ C ∈ l     [X2] by -, Collinear_DEF;
    l = m     by X1, -, H2, H1, I1;
  qed     by -, X2;
`;;

let CollinearLinear = thm `;
  let A B C be point;
  let m be point_set;
  assume Line m ∧ A ∈ m ∧ C ∈ m     [H1];
  assume Collinear A B C ∨ Collinear B C A ∨ Collinear C A B     [H2];
  assume ¬(A = C)     [H3];
  thus B ∈ m

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

let NonCollinearImpliesDistinct = 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     [Case1];
      consider Q such that
      ¬(Q = A)     by I3;
    qed     by -, I1, Case1, Collinear_DEF, H1;
    suppose (A = B ∧ ¬(A = C)) ∨  (A = C ∧ ¬(A = B)) ∨ (B = C ∧ ¬(A = B));
    qed by -, I1, Collinear_DEF, H1;
    suppose ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C);
    qed by -;
  end;
`;;

let Reverse4Order = thm `;
  ∀ A B C D:point. ordered A B C D  ⇒  ordered D C B A
  by Ordered_DEF, B1';
`;;

let OriginInRay = thm `;
  let O Q be point;
  assume ¬(Q = O)     [H1];
  thus O ∈ ray O Q

  proof
    O ∉ open (O,Q)     [OOQ] by B1', ∉;
    Collinear O Q O     by H1, I1, Collinear_DEF;
  qed     by H1, -, OOQ, IN_Ray;
`;;

let EndpointInRay = thm `;
  let O Q be point;
  assume ¬(Q = O)     [H1];
  thus Q ∈ ray O Q

  proof
    O ∉ open (Q,Q)     [notOQQ] by B1', ∉;
    Collinear O Q Q     by H1, I1, Collinear_DEF;
  qed     by H1, -, notOQQ, IN_Ray;
`;;

let I1Uniqueness = thm `;
  let X be point;
  let l m be point_set;
  assume Line l ∧ Line m        [H0];
  assume ¬(l = m)               [H1];
  assume X ∈ l ∧ X ∈ m          [H2];
  thus l ∩ m = {X}

  proof
    assume ¬(l ∩ m = {X})     [H3];
    X ∈ l ∩ m     by H2, IN_INTER;
    consider A such that
    A ∈ l ∩ m  ∧ ¬(A = X)     [X1] by -, H3, SET_RULE;
    A ∈ l ∧ X ∈ l ∧ A ∈ m ∧ X ∈ m     by H0, -, H2, IN_INTER;
    l = m     by H0, -, X1, I1;
  qed     by -, H1;
`;;

let EquivIntersection = thm `;
  let A B X be point;
  let l m be point_set;
  assume Line l ∧ Line m                [H0];
  assume l ∩ m = {X}                    [H1];
  assume A ∈ m ━ X ∧ B ∈ m ━ X          [H2];
  assume X ∉ open (A,B)                 [H3];
  thus  A,B same_side l

  proof
    assume ¬(A,B same_side l) [Con];
    A ∈ m ∧ B ∈ m ∧ ¬(A = X) ∧ ¬(B = X)     [H2'] by H2, IN_DELETE;
    ¬(open (A,B) ∩ l = ∅)     [nonempty] by H0, Con, SameSide_DEF, SET_RULE;
    open (A,B) ⊂ m     [ABm] by H0, H2', BetweenLinear, SUBSET;
    open (A,B) ∩ l  ⊂  {X}     by -, SET_RULE, H1;
    X ∈ open (A,B) ∩ l     by nonempty, -, SET_RULE;
  qed     by -, IN_INTER, H3, ∉;
`;;

let RayLine = thm `;
  ∀ O P:point. ∀ l: point_set.
  Line l ∧ O ∈ l ∧ P ∈ l  ⇒  ray O P  ⊂ l
  by IN_Ray, CollinearLinear, SUBSET;
`;;

let RaySameSide = thm `;
  let l be point_set;
  let O A P be point;
  assume Line l ∧ O ∈ l         [l_line];
  assume A ∉ l                  [notAl];
  assume P ∈ ray O A ━ O                [PrOA];
  thus P ∉ l  ∧  P,A same_side l

  proof
    ¬(O = A)     [notOA] by l_line, notAl, ∉;
    consider d such that
    Line d ∧ O ∈ d ∧ A ∈ d     [d_line] by notOA, I1;
    ¬(l = d)     by -, notAl, ∉;
    l ∩ d = {O}     [ldO] by l_line, d_line, -, I1Uniqueness;
    A ∈ d ━ O     [Ad_O] by d_line, notOA, IN_DELETE;
    ray O A ⊂ d     by d_line, RayLine;
    P ∈ d ━ O     [Pd_O] by PrOA, -, SUBSET, IN_DELETE;
    P ∉ l     [notPl] by ldO, -, EquivIntersectionHelp;
    O ∉ open (P,A)     by PrOA, IN_DELETE, IN_Ray;
    P,A same_side l     by l_line, d_line, ldO, Ad_O, Pd_O, -, EquivIntersection;
  qed     by notPl, -;
`;;

let IntervalRayEZ = thm `;
  let A B C be point;
  assume B ∈ open (A,C)                         [H1];
  thus B ∈ ray A C ━ A  ∧  C ∈ ray A B ━ A

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C     [ABC] by H1, B1';
    A ∉ open (B,C)  ∧  A ∉ open (C,B)     by -, H1, B3', B1', ∉;
  qed     by ABC, CollinearSymmetry, -, IN_Ray, IN_DELETE, ∉;
`;;

let NoncollinearityExtendsToLine = thm `;
  let A O B X be point;
  assume ¬Collinear A O B                       [H1];
  assume Collinear O B X  ∧ ¬(X = O)            [H2];
  thus ¬Collinear A O X

  proof
    ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B)     [Distinct] by H1, NonCollinearImpliesDistinct;
    consider b such that
    Line b ∧ O ∈ b ∧ B ∈ b     [b_line] by Distinct, I1;
    A ∉ b     [notAb] by b_line, Collinear_DEF, H1, ∉;
    X ∈ b     by H2, b_line, Distinct, I1, Collinear_DEF;
  qed     by b_line, -, H2, I1, Collinear_DEF, notAb, ∉;
`;;

let SameSideReflexive = thm `;
  ∀ l A. Line l ∧  A ∉ l ⇒ A,A same_side l
  by B1', SameSide_DEF;
`;;

let SameSideSymmetric = thm `;
  ∀ l A B. Line l ∧  A ∉ l ∧ B ∉ l ⇒
  A,B same_side l ⇒ B,A same_side l
  by SameSide_DEF, B1';
`;;

let SameSideTransitive = thm `;
  let l be point_set;
  let A B C be point;
  assume Line l                         [l_line];
  assume A ∉ l ∧ B ∉ l ∧ C ∉ l          [notABCl];
  assume A,B same_side l                [Asim_lB];
  assume B,C same_side l                [Bsim_lC];
  thus A,C same_side l

  proof
    cases;
    suppose ¬Collinear A B C  ∨  A = B ∨ A = C ∨ B = C;
    qed     by l_line, -, notABCl, Asim_lB, Bsim_lC, B4'', SameSideReflexive;
    suppose Collinear A B C  ∧ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [Distinct];
      consider m such that
      Line m ∧ A ∈ m ∧ C ∈ m     [m_line] by Distinct, I1;
      B ∈ m     [Bm] by -, Distinct, CollinearLinear;
      cases;
      suppose m ∩ l = ∅;
      qed     by m_line, l_line, -, BetweenLinear, SET_RULE, SameSide_DEF;
      suppose ¬(m ∩ l = ∅);
        consider X such that
        X ∈ l ∧ X ∈ m     [Xlm] by -, MEMBER_NOT_EMPTY, IN_INTER;
        Collinear A X B  ∧  Collinear B A C  ∧  Collinear A B C     [ABXcol] by m_line, Bm, -, Collinear_DEF;
        consider E such that
        E ∈ l ∧ ¬(E = X)     [El_X] by l_line, Xlm, ExistsNewPointOnLine;
        ¬Collinear E A X     [EAXncol] by  l_line, El_X, Xlm, I1, Collinear_DEF, notABCl, ∉;
        consider B' such that
        ¬(B = E)  ∧  B ∈ open (E,B')     [EBB'] by notABCl, El_X, ∉, B2';
        ¬(B' = E) ∧ ¬(B' = B) ∧ Collinear B E B'     [EBB'col] by -, B1', CollinearSymmetry;
        ¬Collinear A B B'  ∧  ¬Collinear B' B A  ∧  ¬Collinear B' A B     [ABB'ncol] by EAXncol, ABXcol, Distinct, NoncollinearityExtendsToLine, CollinearSymmetry, -;
        ¬Collinear B' B C ∧  ¬Collinear B' A C ∧  ¬Collinear A B' C     [AB'Cncol] by ABB'ncol, ABXcol, Distinct, NoncollinearityExtendsToLine, CollinearSymmetry;
        B' ∈ ray E B ━ E  ∧  B ∈ ray E B' ━ E     by EBB', IntervalRayEZ;
        B' ∉ l  ∧  B',B same_side l  ∧  B,B' same_side l     [notB'l] by l_line, El_X, notABCl, -, RaySameSide;
        A,B' same_side l ∧  B',C same_side l     by l_line, ABB'ncol, notABCl, notB'l, Asim_lB, -, B4'', AB'Cncol, Bsim_lC;
      qed     by l_line, AB'Cncol, notABCl, notB'l, -, B4'';
    end;
  end;
`;;

let ConverseCrossbar = thm `;
  let O A B G be point;
  assume ¬Collinear A O B     [H1];
  assume G ∈ open (A,B)     [H2];
  thus G ∈ int_angle A O B

  proof
    ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B)     [Distinct] by H1, NonCollinearImpliesDistinct;
    consider a such that
    Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by -, I1;
    consider b such that
    Line b ∧ O ∈ b ∧ B ∈ b     [b_line] by Distinct, I1;
    consider l such that
    Line l ∧ A ∈ l ∧ B ∈ l     [l_line] by Distinct, I1;
     B ∉ a  ∧  A ∉ b     by H1, a_line, Collinear_DEF, ∉, b_line;
    ¬(a = l)  ∧  ¬(b = l)     by -, l_line, ∉;
    a ∩ l = {A}  ∧  b ∩ l = {B}     [alA] by -, a_line, l_line, I1Uniqueness, b_line;
    ¬(A = G) ∧ ¬(A = B) ∧ ¬(G = B)     [AGB] by H2, B1';
    A ∉ open (G,B)  ∧  B ∉ open (G,A)     [notGAB] by H2, B3', B1', ∉;
    G ∈ l     [Gl] by l_line, H2, BetweenLinear;
    G ∉ a  ∧  G ∉ b     [notGa] by alA, Gl, AGB, IN_DELETE, EquivIntersectionHelp;
    G ∈ l ━ A ∧ B ∈ l ━ A ∧ G ∈ l ━ B ∧ A ∈ l ━ B      by Gl, l_line, AGB, IN_DELETE;
    G,B same_side a  ∧  G,A same_side b     by a_line, l_line, alA, -, notGAB, EquivIntersection, b_line;
  qed     by H1, a_line, b_line, notGa, -, IN_InteriorAngle;
`;;

let InteriorUse = thm `;
  let A O B P be point;
  let a b be point_set;
  assume Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b     [aOAbOB];
  assume  P  ∈ int_angle A O B     [P_AOB];
  thus P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b

  proof
    consider α β such that ¬Collinear A O B ∧
    Line α ∧ O ∈ α ∧ A ∈ α ∧
    Line β ∧ O ∈ β ∧B ∈ β ∧
    P ∉ α ∧ P ∉ β ∧
    P,B same_side α ∧ P,A same_side β     [exists] by P_AOB, IN_InteriorAngle;
    ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B)     [Distinct] by -, NonCollinearImpliesDistinct;
    α = a ∧ β = b     by -, aOAbOB, exists, I1;
  qed     by -, exists;
`;;

let InteriorEZHelp = 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 ∈ a ∧ A ∈ a ∧
    Line b ∧ O ∈ b ∧B ∈ b ∧
    P ∉ a ∧ P ∉ b     [def_int] by P_AOB, IN_InteriorAngle;
    ¬(P = A) ∧ ¬(P = O) ∧ ¬(P = B)     [PnotAOB] by -, ∉;
    ¬(A = O)     [notAO] by def_int, NonCollinearImpliesDistinct;
    ¬Collinear A O P by def_int, notAO, -, I1, Collinear_DEF, ∉;
  qed     by PnotAOB, -;
`;;

let InteriorAngleSymmetry = thm `;
  ∀ A O B P: point. P ∈ int_angle A O B  ⇒  P ∈ int_angle B O A
  by IN_InteriorAngle, CollinearSymmetry;
`;;

let InteriorWellDefined = thm `;
  let A O B X P be point;
  assume P ∈ int_angle A O B            [H1];
  assume X ∈ ray O B ━ O                [H2];
  thus P ∈ int_angle A O X

  proof
    consider a b such that
    ¬Collinear A O B ∧
    Line a ∧ O ∈ a ∧ A ∈ a ∧ P ∉ a     ∧     Line b ∧ O ∈ b ∧ B ∈ b ∧ P ∉ b ∧
    P,B same_side a ∧ P,A same_side b     [def_int] by H1, IN_InteriorAngle;
    ¬(X = O) ∧ ¬(O = B) ∧ Collinear O B X     [H2'] by H2, IN_DELETE, IN_Ray;
    B ∉ a     [notBa] by def_int, Collinear_DEF, ∉;
    ¬Collinear A O X     [AOXnoncol] by def_int, H2', NoncollinearityExtendsToLine;
    X ∈ b     [Xb] by def_int, H2', CollinearLinear;
    X ∉ a  ∧  B,X same_side a     by def_int, notBa, H2, RaySameSide, SameSideSymmetric;
    P,X same_side a     by def_int, -, notBa, SameSideTransitive;
  qed     by AOXnoncol, def_int, Xb, -, IN_InteriorAngle;
`;;

let WholeRayInterior = thm `;
  let A O B X P be point;
  assume X ∈ int_angle A O B            [XintAOB];
  assume P ∈ ray O X ━ O                [PrOX];
  thus P ∈ int_angle A O B

  proof
    consider a b such that
    ¬Collinear A O B ∧
    Line a ∧ O ∈ a ∧ A ∈ a ∧ X ∉ a   ∧   Line b ∧ O ∈ b ∧ B ∈ b ∧ X ∉ b ∧
    X,B same_side a ∧ X,A same_side b     [def_int] by XintAOB, IN_InteriorAngle;
    P ∉ a ∧ P,X same_side a ∧ P ∉ b ∧ P,X same_side b     [Psim_abX] by def_int, PrOX, RaySameSide;
    P,B same_side a  ∧ P,A same_side b     by -, def_int, Collinear_DEF, SameSideTransitive, ∉;
  qed     by def_int, Psim_abX, -, IN_InteriorAngle;
`;;

let AngleOrdering = thm `;
  let O A P Q be point;
  let a be point_set;
  assume ¬(O = A)     [H1];
  assume Line a ∧ O ∈ a ∧ A ∈ a                 [H2];
  assume P ∉ a ∧ Q ∉ 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;
    consider q such that
    Line q ∧ O ∈ q ∧ Q ∈ q     [q_line] by Distinct, I1;
    P ∉ q     [notPq] by -, Collinear_DEF, H5, ∉;
    assume ¬(P ∈ int_angle Q O A)     [notPintQOA];
    ¬Collinear Q O A  ∧  ¬Collinear P O A     [POAncol] by H1, H2, I1, Collinear_DEF, H3, ∉;
    ¬(P,A same_side q)     by -, H2, q_line, H3, notPq, H4, notPintQOA, IN_InteriorAngle;
    consider G such that
    G ∈ q ∧ G ∈ open (P,A)     [existG] by q_line, -, SameSide_DEF;
    G ∈ int_angle P O A     [G_POA] by  POAncol, existG, ConverseCrossbar;
    G ∉ a ∧ G,P same_side a ∧ ¬(G = O)    [Gsim_aP] by -, IN_InteriorAngle, H1, H2, I1, ∉;
    G,Q same_side a     by H2, Gsim_aP, H3, H4, SameSideTransitive;
    O ∉ open (Q,G)     [notQOG] by -, SameSide_DEF, H2, B1', ∉;
    Collinear O G Q     by q_line, existG, Collinear_DEF;
    Q ∈ ray O G ━ O     by Gsim_aP, -, notQOG, IN_Ray, Distinct, IN_DELETE;
  qed     by G_POA, -, WholeRayInterior;
`;;

let InteriorsDisjointSupplement = thm `;
  let A O B A' be point;
  assume ¬Collinear A O B                               [H1];
  assume O ∈ open (A,A')                                [H2];
  thus  int_angle B O A'  ∩  int_angle A O B = ∅

  proof
    ∀ D. D ∈ int_angle A O B  ⇒  D ∉ int_angle B O A'
    proof
      let D be point;
      assume D ∈ int_angle A O B     [H3];
      ¬(A = O) ∧ ¬(O = B)     by H1, NonCollinearImpliesDistinct;
      consider a b such that
      Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧ A' ∈ a     [ab_line] by -, I1, H2, BetweenLinear;
      ¬Collinear B O A'     by H1, CollinearSymmetry, H2, B1', NoncollinearityExtendsToLine;
      A ∉ b  ∧  A' ∉ b     [notAb] by ab_line, Collinear_DEF, H1, -, ∉;
      ¬(A',A same_side b)     [A'nsim_bA] by ab_line, H2, B1', SameSide_DEF ;
      D ∉ b  ∧  D,A same_side b     [DintAOB] by ab_line, H3, InteriorUse;
      ¬(D,A' same_side b)     by ab_line, notAb, DintAOB, A'nsim_bA, SameSideSymmetric, SameSideTransitive;
      qed     by ab_line, -, InteriorUse, ∉;
  qed by -, DisjointOneNotOther;
`;;

let InteriorReflectionInterior = thm `;
  let A O B D A' be point;
  assume O ∈ open (A,A')                [H1];
  assume D ∈ int_angle A O B            [H2];
  thus B  ∈ int_angle D O A'

  proof
    consider a b such that
    ¬Collinear A O B ∧ Line a ∧ O ∈ a ∧ A ∈ a ∧ D ∉ a ∧
    Line b ∧ O ∈ b ∧ B ∈ b ∧ D ∉ b ∧ D,B same_side a     [DintAOB] by H2, IN_InteriorAngle;
    ¬(O = B) ∧ ¬(O = A') ∧ B ∉ a     [Distinct] by -, NonCollinearImpliesDistinct, H1, B1', Collinear_DEF, ∉;
    ¬Collinear D O B     [DOB_ncol] by DintAOB, -, I1, Collinear_DEF, ∉;
    A' ∈ a     [A'a] by H1, DintAOB, BetweenLinear;
    D ∉ int_angle B O A'     by DintAOB, H1, InteriorsDisjointSupplement, H2, DisjointOneNotOther;
  qed     by Distinct, DintAOB, A'a, DOB_ncol, -, AngleOrdering, ∉;
`;;

let Crossbar_THM = thm `;
  let O A B D be point;
  assume D ∈ int_angle A O B     [H1];
  thus ∃ G. G ∈ open (A,B)  ∧  G ∈ ray O D ━ O

  proof
    consider a b such that
    ¬Collinear A O B ∧
    Line a ∧ O ∈ a ∧ A ∈ a ∧
    Line b ∧ O ∈ b ∧ B ∈ b ∧
    D ∉ a ∧ D ∉ b ∧ D,B same_side a ∧ D,A same_side b     [DintAOB] by H1, IN_InteriorAngle;
    B ∉ a     [notBa] by DintAOB, Collinear_DEF, ∉;
    ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B) ∧ ¬(D = O)     [Distinct] by DintAOB, NonCollinearImpliesDistinct, ∉;
    consider l such that
    Line l ∧ O ∈ l ∧ D ∈ l     [l_line] by -, I1;
    consider A' such that
    O ∈ open (A,A')     [AOA'] by Distinct, B2';
    A' ∈ a ∧ Collinear A O A' ∧ ¬(A' = O)      [A'a] by DintAOB, -, BetweenLinear, B1';
    ¬(A,A' same_side l)     [Ansim_lA'] by l_line, AOA', SameSide_DEF;
    B ∈ int_angle D O A'     by H1, AOA', InteriorReflectionInterior;
    B,A' same_side l     [Bsim_lA'] by l_line, DintAOB, A'a, -, InteriorUse;
    ¬Collinear A O D  ∧  ¬Collinear B O D      [AODncol] by H1, InteriorEZHelp, InteriorAngleSymmetry;
    ¬Collinear D O A'      by -, CollinearSymmetry, A'a, NoncollinearityExtendsToLine;
    A ∉ l ∧ B ∉ l ∧ A' ∉ l     by l_line, Collinear_DEF, AODncol, -, ∉;
    ¬(A,B same_side l)     by l_line, -, Bsim_lA', Ansim_lA', SameSideTransitive;
    consider G such that
    G ∈ open (A,B) ∧ G ∈ l     [AGB] by l_line, -, SameSide_DEF;
    Collinear O D G     [ODGcol] by -, l_line, Collinear_DEF;
    G ∈ int_angle A O B     by DintAOB, AGB, ConverseCrossbar;
    G ∉ a  ∧  G,B same_side a  ∧  ¬(G = O)     [Gsim_aB] by DintAOB, -, InteriorUse, ∉;
    B,D same_side a     by DintAOB, notBa, SameSideSymmetric;
    G,D same_side a     [Gsim_aD] by DintAOB, Gsim_aB, notBa, -, SameSideTransitive;
    O ∉ open (G,D)     by DintAOB, -, SameSide_DEF, ∉;
    G ∈ ray O D ━ O     by Distinct, ODGcol, -, IN_Ray, Gsim_aB, IN_DELETE;
  qed     by AGB, -;
`;;

let AlternateConverseCrossbar = thm `;
  let O A B G be point;
  assume Collinear A G B  ∧  G ∈ int_angle A O B                [H1];
  thus G ∈ open (A,B)

  proof
    consider a b such that
    ¬Collinear A O B  ∧  Line a ∧ O ∈ a ∧ A ∈ a  ∧  Line b ∧ O ∈ b ∧ B ∈ b  ∧
    G,B same_side a  ∧  G,A same_side b     [GintAOB] by H1, IN_InteriorAngle;
    ¬(A = B) ∧ ¬(G = A) ∧ ¬(G = B)  ∧  A ∉ open (G,B)  ∧  B ∉ open (G,A)     by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp, SameSide_DEF, ∉;
  qed     by -, H1, B1', B3', ∉;
`;;

let InteriorOpposite = thm `;
  let A O B P be point;
  let p be point_set;
  assume P ∈ int_angle A O B            [PintAOB];
  assume Line p ∧ O ∈ p ∧ P ∈ p         [p_line];
  thus ¬(A,B same_side p)

  proof
    consider G such that
    G ∈ open (A,B) ∧ G ∈ ray O P     [Gexists] by PintAOB, Crossbar_THM, IN_DELETE;
    G ∈ p     by p_line, RayLine, -, SUBSET;
  qed     by p_line, -, Gexists, SameSide_DEF;
`;;

let IntervalTransitivity = thm `;
  let O P Q R be point;
  let m be point_set;
  assume Line m  ∧ O ∈ m                                [H0];
  assume P ∈ m ━ O ∧ Q ∈ m ━ O ∧ R ∈ m ━ O      [H2];
  assume O ∉ open (P,Q) ∧ O ∉ open (Q,R)                [H3];
  thus O ∉ open (P,R)

  proof
    consider E such that
    E ∉ m ∧  ¬(O = E)     [notEm] by H0, ExistsPointOffLine, ∉;
    consider l such that
    Line l ∧ O ∈ l ∧ E ∈ l     [l_line] by -, I1;
    ¬(m = l)     by notEm, -, ∉;
    l ∩ m = {O}     [lmO] by l_line, H0, -, l_line, I1Uniqueness;
    P ∉ l ∧  Q ∉ l ∧ R ∉ l     [notPQRl] by -, H2, EquivIntersectionHelp;
    P,Q same_side l  ∧  Q,R same_side l     by l_line, H0, lmO, H2, H3, EquivIntersection;
    P,R same_side l     [Psim_lR] by l_line, notPQRl, -, SameSideTransitive;
  qed     by l_line, -, SameSide_DEF, ∉;
`;;

let RayWellDefinedHalfway = thm `;
  let O P Q be point;
  assume ¬(Q = O)               [H1];
  assume P ∈ ray O Q ━ O        [H2];
  thus ray O P ⊂ ray O Q

  proof
    consider m such that
    Line m ∧ O ∈ m ∧ Q ∈ m     [OQm] by H1, I1;
    P ∈ ray O Q  ∧  ¬(P = O)  ∧  O ∉ open (P,Q)     [H2'] by H2, IN_DELETE, IN_Ray;
    P ∈ m  ∧  P ∈ m ━ O  ∧  Q ∈ m ━ O     [PQm_O] by OQm, H2', RayLine, SUBSET, H2', OQm, H1, IN_DELETE;
    O ∉ open (P,Q)     [notPOQ] by H2', IN_Ray;
    ∀ X. X ∈ ray O P ⇒ X ∈ ray O Q
    proof
      let X be point;
      assume X ∈ ray O P;
      X ∈ m  ∧  O ∉ open (X,P)     [XrOP] by OQm, PQm_O, H2', -, RayLine, SUBSET, IN_Ray;
      Collinear O Q X     [OQXcol] by OQm, -,  Collinear_DEF;
      cases;
      suppose X = O;
      qed     by H1, -, OriginInRay;
      suppose ¬(X = O);
        X ∈ m ━ O     by XrOP, -, IN_DELETE;
        O ∉ open (X,Q)     by OQm, -, PQm_O, XrOP, H2', IntervalTransitivity;
      qed     by H1, OQXcol, -, IN_Ray;
    end;
  qed     by -, SUBSET;
`;;

let RayWellDefined = thm `;
  let O P Q be point;
  assume ¬(Q = O)                       [H1];
  assume P ∈ ray O Q ━ O                [H2];
  thus ray O P = ray O Q

  proof
    ray O P ⊂ ray O Q     [PsubsetQ] by H1, H2, RayWellDefinedHalfway;
    ¬(P = O)  ∧  Collinear O Q P  ∧  O ∉ open (P,Q)     [H2'] by H2, IN_DELETE, IN_Ray;
    Q ∈ ray O P ━ O     by H2', B1', ∉, CollinearSymmetry, IN_Ray, H1, IN_DELETE;
    ray O Q ⊂ ray O P     [QsubsetP] by H2', -, RayWellDefinedHalfway;
  qed     by PsubsetQ, QsubsetP, SUBSET_ANTISYM;
`;;

let OppositeRaysIntersect1pointHelp = thm `;
  let A O B X be point;
  assume O ∈ open (A,B)                 [H1];
  assume X ∈ ray O B ━ O                        [H2];
  thus X ∉ ray O A  ∧  O ∈ open (X,A)

  proof
    ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B) ∧ Collinear A O B     [AOB] by H1, B1';
    ¬(X = O) ∧ Collinear O B X ∧ O ∉ open (X,B)     [H2'] by H2, IN_DELETE, IN_Ray;
    consider m such that
    Line m ∧ A ∈ m ∧ B ∈ m     [m_line] by AOB, I1;
    O ∈ m  ∧ X ∈ m     [Om] by m_line, H2', AOB, CollinearLinear;
    A ∈ m ━ O  ∧  X ∈ m ━ O  ∧  B ∈ m ━ O     by m_line, -, H2', AOB, IN_DELETE;
    O ∈ open (X,A)     by H1, m_line, Om, -, H2', IntervalTransitivity, ∉, B1';
  qed     by -, IN_Ray, ∉;
`;;

let OppositeRaysIntersect1point = thm `;
  let A O B be point;
  assume O ∈ open (A,B)                 [H1];
  thus ray O A ∩ ray O B  =  {O}

  proof
    ¬(A = O) ∧ ¬(O = B)     by H1, B1';
    {O}  ⊂  ray O A ∩ ray O B     [Osubset_rOA] by -, OriginInRay, IN_INTER, SING_SUBSET;
    ∀ X. ¬(X = O)  ∧  X ∈ ray O B  ⇒  X ∉ ray O A
    by IN_DELETE, H1, OppositeRaysIntersect1pointHelp;
    ray O A ∩ ray O B  ⊂  {O}     by -, IN_INTER, IN_SING, SUBSET, ∉;
  qed     by -, Osubset_rOA, SUBSET_ANTISYM;
`;;

let IntervalRay = thm `;
  ∀ A B C:point. B ∈ open (A,C)  ⇒  ray A B = ray A C
  by B1', IntervalRayEZ, RayWellDefined;
`;;

let TransitivityBetweennessHelp = thm `;
  let A B C D be point;
  assume B ∈ open (A,C)  ∧  C ∈ open (B,D)     [H1];
  thus B ∈ open (A,D)

  proof
    D ∈ ray B C ━ B     by H1, IntervalRayEZ;
  qed     by H1, -, OppositeRaysIntersect1pointHelp, B1';
`;;

let TransitivityBetweenness = thm `;
  let A B C D be point;
  assume B ∈ open (A,C)  ∧  C ∈ open (B,D)     [H1];
  thus ordered A B C D

  proof
    B ∈ open (A,D)     [ABD] by H1, TransitivityBetweennessHelp;
    C ∈ open (D,B)  ∧  B ∈ open (C,A)     by H1, B1';
    C ∈ open (D,A)     by -, TransitivityBetweennessHelp;
  qed     by H1, ABD, -, B1', Ordered_DEF;
`;;

let IntervalsAreConvex = thm `;
 let A B C be point;
  assume B ∈ open (A,C)         [H1];
  thus open (A,B)  ⊂  open (A,C)

  proof
    ∀ X. X ∈ open (A,B)  ⇒  X ∈ open (A,C)
    proof
      let X be point;
      assume X ∈ open (A,B)     [AXB];
      X ∈ ray B A ━ B     by AXB, B1', IntervalRayEZ;
      B ∈ open (X,C)     by H1, B1', -, OppositeRaysIntersect1pointHelp;
    qed     by AXB, -, TransitivityBetweennessHelp;
  qed     by -, SUBSET;
`;;

let TransitivityBetweennessVariant = thm `;
  let A X B C be point;
  assume X ∈ open (A,B)  ∧  B ∈ open (A,C)     [H1];
  thus ordered A X B C

  proof
    X ∈ ray B A ━ B     by H1, B1', IntervalRayEZ;
    B ∈ open (X,C)     by H1, B1', -, OppositeRaysIntersect1pointHelp;
  qed     by H1, -, TransitivityBetweenness;
`;;

let Interval2sides2aLineHelp = thm `;
  let A B C X be point;
  assume B ∈ open (A,C)                 [H1];
  thus X ∉ open (A,B) ∨ X ∉ open (B,C)

  proof
    assume ¬(X ∉ open (A,B));
    ordered A X B C     by -, ∉, H1, TransitivityBetweennessVariant;
    B ∈ open (X,C)     by -, Ordered_DEF;
    X ∉ open (C,B)     by -, B1', B3', ∉;
  qed     by -, B1', ∉;
`;;

let Interval2sides2aLine = thm `;
  let A B C X be point;
  assume Collinear A B C     [H1];
  thus X ∉ open (A,B)  ∨  X ∉ open (A,C)  ∨  X ∉ open (B,C)

  proof
    cases;
    suppose A = B  ∨  A = C  ∨  B = C;
    qed by -, B1', ∉;
    suppose ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C);
      B ∈ open (A,C)  ∨  C ∈ open (B,A)  ∨  A ∈ open (C,B)     by -, H1, B3';
    qed     by -, Interval2sides2aLineHelp, B1', ∉;
  end;
`;;

let TwosidesTriangle2aLine = thm `;
  let A B C Y be point;
  let l m be point_set;
  assume Line l ∧ ¬Collinear A B C                              [H1];
  assume A ∉ l ∧ B ∉ l ∧ C ∉ l                                 [off_l];
  assume Line m ∧ A ∈ m ∧ C ∈ m                                 [m_line];
  assume Y ∈ l ∧ Y ∈ m                                          [Ylm];
  assume ¬(A,B same_side l) ∧ ¬(B,C same_side l)                [H2];
  thus A,C same_side l

  proof
    consider X Z such that
    X ∈ l  ∧  X ∈ open (A,B)  ∧  Z ∈ l  ∧  Z ∈ open (C,B)     [H2'] by H1, H2, SameSide_DEF, B1';
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Y ∈ m ━ A  ∧  Y ∈ m ━ C  ∧  C ∈ m ━ A  ∧  A ∈ m ━ C     [Distinct] by H1, NonCollinearImpliesDistinct, Ylm, off_l, ∉, m_line, IN_DELETE;
    consider p such that
    Line p ∧ B ∈ p ∧ A ∈ p     [p_line] by Distinct, I1;
    consider q such that
    Line q ∧ B ∈ q ∧ C ∈ q     [q_line] by Distinct, I1;
    X ∈ p  ∧ Z ∈ q     [Xp] by p_line, H2', BetweenLinear, q_line, H2';
    A ∉ q ∧ B ∉ m ∧ C ∉ p     [vertex_off_line] by q_line, m_line, p_line, H1, Collinear_DEF, ∉;
    X ∉ q  ∧  X,A same_side q  ∧  Z ∉ p  ∧  Z,C same_side p     [Xsim_qA] by q_line, p_line, -, H2', B1', IntervalRayEZ, RaySameSide;
    ¬(m = p)  ∧  ¬(m = q)     by m_line, vertex_off_line, ∉;
    p ∩ m = {A}  ∧  q ∩ m = {C}     [pmA] by p_line, m_line, q_line, H1, -, Xp, H2', I1Uniqueness;
    Y ∉ p  ∧  Y ∉ q     [notYpq] by -, Distinct, EquivIntersectionHelp;
    X ∈ ray A B ━ A  ∧  Z ∈ ray C B ━ C     by H2', IntervalRayEZ, H2', B1';
    X ∉ m  ∧  Z ∉ m  ∧  X,B same_side m  ∧  B,Z same_side m     [notXZm] by m_line, vertex_off_line, -, RaySameSide, SameSideSymmetric;
    X,Z same_side m     by m_line, -, vertex_off_line, SameSideTransitive;
    Collinear X Y Z ∧ Y ∉ open (X,Z) ∧  ¬(Y = X) ∧ ¬(Y = Z) ∧ ¬(X = Z)     by H1, H2', Ylm, Collinear_DEF, m_line, -, SameSide_DEF, notXZm, Xsim_qA, Xp, ∉;
    Z ∈ open (X,Y)  ∨  X ∈ open (Z,Y)     by -, B3', ∉, B1';
    cases     by -;
    suppose X ∈ open (Z,Y);
      ¬(Z,Y same_side p)     by p_line, Xp, -, SameSide_DEF;
      ¬(C,Y same_side p)     by p_line, Xsim_qA, vertex_off_line, notYpq, -, SameSideTransitive;
      A ∈ open (C,Y)     by p_line, m_line, pmA, Distinct, -, EquivIntersection, ∉;
    qed     by H1, Ylm, off_l, -, B1', IntervalRayEZ, RaySameSide;
    suppose Z ∈ open (X,Y);
      ¬(X,Y same_side q)     by q_line, Xp, -, SameSide_DEF;
      ¬(A,Y same_side q)     by q_line, Xsim_qA, vertex_off_line, notYpq, -, SameSideTransitive;
      C ∈ open (Y,A)     by q_line, m_line, pmA, Distinct, -, EquivIntersection, ∉, B1';
    qed     by H1, Ylm, off_l, -, IntervalRayEZ, RaySameSide;
  end;
`;;

let LineUnionOf2Rays = thm `;
  let A O B be point;
  let l be point_set;
  assume Line l ∧ A ∈ l ∧ B ∈ l         [H1];
  assume O ∈ open (A,B)                 [H2];
  thus l = ray O A ∪ ray O B

  proof
    ¬(A = O) ∧ ¬(O = B) ∧ O ∈ l     [Distinct] by H2, B1', H1, BetweenLinear;
    ray O A ∪ ray O B  ⊂  l     [AOBsub_l] by H1, -, RayLine, UNION_SUBSET;
    ∀ X. X ∈ l  ⇒  X ∈ ray O A  ∨  X ∈ ray O B
    proof
      let X be point;
      assume X ∈ l     [Xl];
      assume ¬(X ∈ ray O B)     [notXrOB];
      Collinear O B X  ∧  Collinear X A B  ∧  Collinear O A X     [XABcol] by Distinct, H1, Xl, Collinear_DEF;
      O ∈ open (X,B)     by notXrOB, Distinct, -, IN_Ray, ∉;
      O ∉ open (X,A)     by ∉, B1', XABcol, -, H2, Interval2sides2aLine;
    qed     by Distinct, XABcol, -, IN_Ray;
    l ⊂ ray O A ∪ ray O B     by -, IN_UNION, SUBSET;
  qed     by -, AOBsub_l, SUBSET_ANTISYM;
`;;

let AtMost2Sides = thm `;
  let A B C be point;
  let l be point_set;
  assume Line l                                                         [H1];
  assume A ∉ l ∧ B ∉ l ∧ C ∉ l                                          [H2];
  thus A,B same_side l  ∨  A,C same_side l  ∨  B,C same_side l

  proof
    cases;
    suppose A = C;
    qed     by -, H1, H2, SameSideReflexive;
    suppose ¬(A = C)     [notAC];
      consider m such that
      Line m ∧ A ∈ m ∧ C ∈ m     [m_line] by notAC, I1;
      cases;
      suppose m ∩ l = ∅;
        A,C same_side l     by m_line, H1, -, BetweenLinear, SET_RULE, SameSide_DEF;
      qed     by -;
      suppose ¬(m ∩ l = ∅);
        consider Y such that
        Y ∈ l ∧ Y ∈ m     [Ylm] by -, IN_INTER, MEMBER_NOT_EMPTY;
        cases;
        suppose ¬Collinear A B C;
        qed     by H1, -, H2, m_line, Ylm, TwosidesTriangle2aLine;
        suppose Collinear A B C     [ABCcol];
          B ∈ m     [Bm] by -, m_line, notAC, I1, Collinear_DEF;
          ¬(Y = A) ∧ ¬(Y = B) ∧ ¬(Y = C)     [YnotABC] by Ylm, H2, ∉;
          Y ∉ open (A,B)  ∨  Y ∉ open (A,C)  ∨  Y ∉ open (B,C)     by ABCcol, Interval2sides2aLine;
          A ∈ ray Y B ━ Y  ∨  A ∈ ray Y C ━ Y  ∨  B ∈ ray Y C ━ Y     by YnotABC, m_line, Bm, Ylm, Collinear_DEF, -, IN_Ray, IN_DELETE;
        qed     by H1, Ylm, H2, -, RaySameSide;
      end;
    end;
  end;
`;;

let FourPointsOrder = thm `;
  let A B C X be point;
  let l be point_set;
  assume Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ X ∈ l         [H1];
  assume ¬(X = A) ∧ ¬(X = B) ∧ ¬(X = C)                 [H2];
  assume B ∈ open (A,C)                                 [H3];
  thus ordered X A B C  ∨  ordered A X B C  ∨
       ordered A B X C  ∨  ordered A B C X

  proof
    A ∈ open (X,B)  ∨  X ∈ open (A,B)  ∨  X ∈ open (B,C)  ∨  C ∈ open (B,X)
    proof
      ¬(A = B) ∧ ¬(B = C)    [ABCdistinct] by H3, B1';
      Collinear A B X ∧ Collinear A C X ∧ Collinear C B X     [ACXcol] by H1, Collinear_DEF;
      A ∈ open (X,B)  ∨  X ∈ open (A,B)  ∨  B ∈ open (A,X)     by H2, ABCdistinct, -, B3', B1';
      cases     by -;
      suppose A ∈ open (X,B) ∨ X ∈ open (A,B);
      qed     by -;
      suppose B ∈ open (A,X);
        B ∉ open (C,X)     by ACXcol, H3, -, Interval2sides2aLine, ∉;
      qed     by H2, ABCdistinct, ACXcol, -, B3', B1', ∉;
    end;
    qed by -, H3, B1', TransitivityBetweenness, TransitivityBetweennessVariant, Reverse4Order;
`;;

let HilbertAxiomRedundantByMoore = thm `;
  let A B C D be point;
  let l be point_set;
  assume Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ D ∈ l                         [H1];
  assume ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D)        [H2];
  thus ordered D A B C ∨ ordered A D B C ∨ ordered A B D C ∨ ordered A B C D ∨
       ordered D A C B ∨ ordered A D C B ∨ ordered A C D B ∨ ordered A C B D ∨
       ordered D C A B ∨ ordered C D A B ∨ ordered C A D B ∨ ordered C A B D

  proof
    Collinear A B C     by H1, Collinear_DEF;
    B ∈ open (A,C)  ∨  C ∈ open (A,B)  ∨  A ∈ open (C,B)     by H2, -, B3', B1';
  qed     by -, H1, H2, FourPointsOrder;
`;;

let InteriorTransitivity = thm `;
  let A O B F G be point;
  assume G ∈ int_angle A O B     [GintAOB];
  assume F ∈ int_angle A O G     [FintAOG];
  thus F ∈ int_angle A O B

  proof
    ¬Collinear A O B     [AOBncol] by GintAOB, IN_InteriorAngle;
    consider G' such that
    G' ∈ open (A,B)  ∧  G' ∈ ray O G ━ O     [CrossG] by GintAOB, Crossbar_THM;
    F ∈ int_angle A O G'     by FintAOG, -, InteriorWellDefined;
    consider F' such that
    F' ∈ open (A,G')  ∧  F' ∈ ray O F ━ O     [CrossF] by -, Crossbar_THM;
    ¬(F' = O) ∧ ¬(F = O) ∧ Collinear O F F' ∧ O ∉ open (F',F)     by -, IN_DELETE, IN_Ray;
    F ∈ ray O F' ━ O     [FrOF'] by -, CollinearSymmetry, B1', ∉, IN_Ray, IN_DELETE;
    open (A,G') ⊂ open (A,B)  ∧  F' ∈ open (A,B)     by CrossG, IntervalsAreConvex, CrossF, SUBSET;
    F' ∈ int_angle A O B     by AOBncol, -, ConverseCrossbar;
  qed     by -, FrOF', WholeRayInterior;
`;;

let HalfPlaneConvexNonempty = thm `;
  let l H be point_set;
  let A be point;
  assume Line l ∧ A ∉ l                         [l_line];
  assume H = {X | X ∉ l  ∧  X,A same_side l}            [HalfPlane];
  thus ¬(H = ∅)  ∧  H ⊂ complement l  ∧  Convex H

  proof
    ∀ X. X ∈ H  ⇔  X ∉ l  ∧  X,A same_side l     [Hdef] by HalfPlane, SET_RULE;
    H ⊂ complement l     [Hsub] by -, IN_PlaneComplement, SUBSET;
    A,A same_side l  ∧  A ∈ H     by l_line, SameSideReflexive, Hdef;
    ¬(H = ∅)     [Hnonempty] by -, MEMBER_NOT_EMPTY;
    ∀ P Q X.  P ∈ H ∧ Q ∈ H ∧ X ∈ open (P,Q)  ⇒  X ∈ H
    proof
      let  P Q X be point;
      assume P ∈ H ∧ Q ∈ H ∧ X ∈ open (P,Q)     [PXQ];
      P ∉ l  ∧  P,A same_side l  ∧  Q ∉ l  ∧  Q,A same_side l     [PQinH] by -, Hdef;
      P,Q same_side l     [Psim_lQ] by l_line, -, SameSideSymmetric, SameSideTransitive;
      X ∉ l     [notXl] by -, PXQ, SameSide_DEF, ∉;
      open (X,P) ⊂ open (P,Q)     by PXQ, IntervalsAreConvex, B1', SUBSET;
      X,P same_side l     by l_line, -, SUBSET, Psim_lQ, SameSide_DEF;
      X,A same_side l     by l_line, notXl, PQinH, -, Psim_lQ, PQinH, SameSideTransitive;
    qed     by -, notXl, Hdef;
    Convex H     by -, SUBSET, CONVEX;
  qed     by Hnonempty, Hsub, -;
`;;

let PlaneSeparation = thm `;
  let l be point_set;
  assume Line l                                                 [l_line];
  thus ∃ H1 H2:point_set. H1 ∩ H2 = ∅  ∧  ¬(H1 = ∅)  ∧  ¬(H2 = ∅)  ∧
         Convex H1  ∧  Convex H2  ∧  complement l = H1 ∪ H2  ∧
         ∀ P Q. P ∈ H1 ∧ Q ∈ H2  ⇒  ¬(P,Q same_side l)

  proof
    consider A such that
    A ∉ l     [notAl] by l_line, ExistsPointOffLine;
    consider E such that
    E ∈ l  ∧  ¬(A = E)     [El] by l_line, I2, -, ∉;
    consider B such that
    E ∈ open (A,B)  ∧  ¬(E = B)  ∧  Collinear A E B     [AEB] by -, B2', B1';
    B ∉ l     [notBl] by l_line, El, -, I1, Collinear_DEF, notAl, ∉;
    ¬(A,B same_side l)     [Ansim_lB] by l_line, El, AEB, SameSide_DEF;
    consider H1 H2 such that
    H1 = {X | X ∉ l  ∧  X,A same_side l}  ∧  H2 = {X | X ∉ l  ∧  X,B same_side l}     [H12sets];
    ∀ X. (X ∈ H1  ⇔  X ∉ l ∧ X,A same_side l) ∧ (X ∈ H2  ⇔  X ∉ l ∧ X,B same_side l)     [H12def] by -, SET_RULE;
    ∀ X. X ∈ H1  ⇔  X ∉ l  ∧  X,A same_side l     [H1def] by H12sets, SET_RULE;
    ∀ X. X ∈ H2  ⇔  X ∉ l  ∧  X,B same_side l     [H2def] by H12sets, SET_RULE;
    H1 ∩ H2 = ∅     [H12disjoint]
    proof
      assume ¬(H1 ∩ H2 = ∅);
      consider V such that
      V ∈ H1 ∧ V ∈ H2     by -, MEMBER_NOT_EMPTY, IN_INTER;
      V ∉ l  ∧  V,A same_side l  ∧  V ∉ l  ∧  V,B same_side l     by -, H12def;
      A,B same_side l     by l_line, -, notAl, notBl, SameSideSymmetric, SameSideTransitive;
    qed     by -, Ansim_lB;
    ¬(H1 = ∅) ∧ ¬(H2 = ∅) ∧ H1 ⊂ complement l ∧ H2 ⊂ complement l ∧ Convex H1 ∧ Convex H2     [H12convex_nonempty] by l_line, notAl, notBl, H12sets, HalfPlaneConvexNonempty;
    H1 ∪ H2  ⊂  complement l     [H12sub] by H12convex_nonempty, UNION_SUBSET;
    ∀ C. C ∈ complement l  ⇒  C ∈ H1 ∪ H2
    proof
      let C be point;
      assume C ∈ complement l;
      C ∉ l     [notCl] by -, IN_PlaneComplement;
      C,A same_side l  ∨  C,B same_side l     by l_line, notAl, notBl, -, Ansim_lB, AtMost2Sides;
      C ∈ H1  ∨  C ∈ H2     by notCl, -, H12def;
    qed     by -, IN_UNION;
    complement l  ⊂  H1 ∪ H2     by -, SUBSET;
    complement l  =  H1 ∪ H2     [compl_H1unionH2] by H12sub, -, SUBSET_ANTISYM;
    ∀ P Q. P ∈ H1 ∧ Q ∈ H2  ⇒  ¬(P,Q same_side l)     [opp_sides]
    proof
      let P Q be point;
      assume P ∈ H1 ∧ Q ∈ H2;
      P ∉ l  ∧  P,A same_side l  ∧   Q ∉ l  ∧  Q,B same_side l     [PH1_QH2] by -, H12def, IN;
    qed     by l_line, -, notAl, SameSideSymmetric, notBl, Ansim_lB, SameSideTransitive;
  qed     by H12disjoint, H12convex_nonempty, compl_H1unionH2, opp_sides;
`;;

let TetralateralSymmetry = thm `;
  let A B C D be point;
  assume Tetralateral A B C D     [H1];
  thus Tetralateral B C D A ∧ Tetralateral A B D C

  proof
     ¬Collinear A B D ∧ ¬Collinear B D C ∧ ¬Collinear D C A ∧ ¬Collinear C A B      [TetraABCD] by H1, Tetralateral_DEF, CollinearSymmetry;
  qed     by H1, -, Tetralateral_DEF;
`;;

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

  proof
    ∀ X. X ∈ open (B,C)  ⇒  X ∉ open (A,B)
    proof
      let X be point;
      assume X ∈ open (B,C);
      ¬Collinear A B C ∧ Collinear B X C ∧ ¬(X = B)     by H1, Tetralateral_DEF, -, B1';
      ¬Collinear A X B     by -, CollinearSymmetry, B1', NoncollinearityExtendsToLine;
    qed by -, B1', ∉;
  qed by -, DisjointOneNotOther;
`;;

let EasyEmptyIntersectionsTetralateral = thm `;
  let A B C D be point;
  assume Tetralateral A B C D                                           [H1];
  thus open (A,B) ∩ open (B,C) = ∅  ∧  open (B,C) ∩ open (C,D) = ∅  ∧
       open (C,D) ∩ open (D,A) = ∅  ∧  open (D,A) ∩ open (A,B) = ∅

  proof
    Tetralateral B C D A  ∧ Tetralateral C D A B  ∧ Tetralateral D A B C by H1, TetralateralSymmetry;
  qed by H1, -, EasyEmptyIntersectionsTetralateralHelp;
`;;

let SegmentSameSideOppositeLine = 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 ∈ a ∧ B ∈ a         [a_line];
  assume Line c ∧ C ∈ c ∧ D ∈ c         [c_line];
  thus A,B same_side c  ∨  C,D same_side a

  proof
    assume ¬(C,D same_side a);     :: prove A,B same_side c
    consider G such that
    G ∈ a ∧ G ∈ open (C,D)     [CGD] by -, a_line, SameSide_DEF;
    G ∈ c ∧ Collinear G B A     [Gc] by c_line, -, BetweenLinear, a_line, Collinear_DEF;
    ¬Collinear B C D  ∧  ¬Collinear C D A  ∧  open (A,B) ∩ open (C,D) = ∅     [quadABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
    A ∉ c ∧ B ∉ c ∧ ¬(A = G) ∧ ¬(B = G)     [Distinct] by -, c_line, Collinear_DEF, ∉, Gc;
    G ∉ open (A,B)     by quadABCD, CGD, DisjointOneNotOther;
    A ∈ ray G B ━ G      by Distinct, Gc, -, IN_Ray, IN_DELETE;
  qed     by c_line, Gc, Distinct, -, RaySameSide;
`;;

let ConvexImpliesQuad = thm `;
  let A B C D be point;
  assume Tetralateral A B C D                                   [H1];
  assume C ∈ int_angle D A B  ∧  D ∈ int_angle A B C            [H2];
  thus Quadrilateral A B C D

  proof
    ¬(A = B) ∧ ¬(B = C) ∧ ¬(A = D)     [TetraABCD] by H1, Tetralateral_DEF;
    consider a such that
    Line a ∧ A ∈ a ∧ B ∈ a     [a_line] by TetraABCD, I1;
    consider b such that
    Line b ∧ B ∈ b ∧ C ∈ b     [b_line] by TetraABCD, I1;
    consider d such that
    Line d ∧ D ∈ d ∧ A ∈ d     [d_line] by TetraABCD, I1;
    open (B,C) ⊂ b  ∧  open (A,B) ⊂ a     [BCbABa] by b_line, a_line, BetweenLinear, SUBSET;
    D,A same_side b  ∧  C,D same_side a     by H2, a_line, b_line, d_line, InteriorUse;
    b ∩ open (D,A) = ∅  ∧  a ∩ open (C,D) = ∅     by -, b_line, SameSide_DEF,  SET_RULE;
    open (B,C) ∩ open (D,A) = ∅  ∧  open (A,B) ∩ open (C,D) = ∅     by BCbABa, -, SET_RULE;
  qed     by H1, -, Quadrilateral_DEF;
`;;

let DiagonalsIntersectImpliesConvexQuad = thm `;
  let A B C D G be point;
  assume ¬Collinear B C D               [BCDncol];
  assume G ∈ open (A,C)  ∧  G ∈ open (B,D)              [DiagInt];
  thus ConvexQuadrilateral A B C D

  proof
    ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D) ∧ ¬(C = A) ∧ ¬(A = G) ∧ ¬(D = G) ∧ ¬(B = G)     [Distinct] by BCDncol, NonCollinearImpliesDistinct, DiagInt, B1';
    Collinear A G C ∧ Collinear B G D     [AGCcol] by DiagInt, B1';
    ¬Collinear C D A     [CDAncol] by BCDncol, CollinearSymmetry, Distinct, AGCcol,  NoncollinearityExtendsToLine;
    ¬Collinear D A B     [DABncol] by -, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine;
    ¬Collinear A B C     [ABCncol] by -, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine;
    ¬(A = B) ∧ ¬(A = D)     by DABncol, NonCollinearImpliesDistinct;
    Tetralateral A B C D     [TetraABCD] by Distinct, -, BCDncol, CDAncol, DABncol, ABCncol, Tetralateral_DEF;
    A ∈ ray C G ━ C  ∧  B ∈ ray D G ━ D  ∧  C ∈ ray A G ━ A  ∧  D ∈ ray B G ━ B     [ArCG] by DiagInt, B1', IntervalRayEZ;
    G ∈ int_angle B C D ∧ G ∈ int_angle C D A ∧ G ∈ int_angle D A B ∧ G ∈ int_angle A B C     by BCDncol, CDAncol, DABncol, ABCncol, DiagInt, B1', ConverseCrossbar;
    A ∈ int_angle B C D ∧ B ∈ int_angle C D A ∧ C ∈ int_angle D A B ∧ D ∈ int_angle A B C     by -, ArCG, WholeRayInterior;
  qed         by TetraABCD, -, ConvexImpliesQuad, ConvexQuad_DEF;
`;;

let DoubleNotSimImpliesDiagonalsIntersect = thm `;
  let A B C D be point;
  let l m be point_set;
  assume Line l ∧ A ∈ l ∧ C ∈ l         [l_line];
  assume Line m ∧ B ∈ m ∧ D ∈ m         [m_line];
  assume Tetralateral A B C D                   [H1];
  assume ¬(B,D same_side l)                     [H2];
  assume ¬(A,C same_side m)                     [H3];
  thus (∃ G. G ∈ open (A,C) ∩ open (B,D)) ∧ ConvexQuadrilateral A B C D

  proof
    ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B     [TetraABCD] by H1, Tetralateral_DEF;
    consider G such that
    G ∈ open (A,C) ∧ G ∈ m     [AGC] by H3, m_line, SameSide_DEF;
    G ∈ l     [Gl] by l_line, -, BetweenLinear;
    A ∉ m ∧ B ∉ l ∧ D ∉ l     by TetraABCD, m_line, l_line, Collinear_DEF, ∉;
    ¬(l = m) ∧ B ∈ m ━ G ∧ D ∈ m ━ G     [BDm_G] by -, l_line, ∉, m_line, Gl, IN_DELETE;
    l ∩ m = {G}     by l_line, m_line, -, Gl, AGC, I1Uniqueness;
    G ∈ open (B,D)     by l_line, m_line, -, BDm_G, H2, EquivIntersection, ∉;
  qed     by AGC, -, IN_INTER, TetraABCD, DiagonalsIntersectImpliesConvexQuad;
`;;

let ConvexQuadImpliesDiagonalsIntersect = thm `;
  let A B C D be point;
  let l m be point_set;
  assume Line l ∧ A ∈ l ∧ C ∈ l                                 [l_line];
  assume Line m ∧ B ∈ m ∧ D ∈ m                                 [m_line];
  assume ConvexQuadrilateral A B C D                                    [ConvQuadABCD];
  thus ¬(B,D same_side l) ∧ ¬(A,C same_side m) ∧
       (∃ G. G ∈ open (A,C) ∩ open (B,D)) ∧ ¬Quadrilateral A B D C

  proof
    Tetralateral A B C D ∧ A ∈ int_angle B C D ∧ D ∈ int_angle A B C     [convquadABCD] by ConvQuadABCD, ConvexQuad_DEF, Quadrilateral_DEF;
    ¬(B,D same_side l)  ∧  ¬(A,C same_side m)     [opp_sides] by convquadABCD, l_line, m_line, InteriorOpposite;
    consider G such that
    G ∈ open (A,C) ∩ open (B,D)     [Gexists] by l_line, m_line, convquadABCD, opp_sides, DoubleNotSimImpliesDiagonalsIntersect;
    ¬(open (B,D) ∩ open (C,A) = ∅)     by -, IN_INTER, B1', MEMBER_NOT_EMPTY;
    ¬Quadrilateral A B D C     by -, Quadrilateral_DEF;
  qed     by opp_sides, Gexists, -;
`;;

let FourChoicesTetralateralHelp = thm `;
  let A B C D be point;
  assume Tetralateral A B C D                                   [H1];
  assume C ∈ int_angle D A B                                    [CintDAB];
  thus ConvexQuadrilateral A B C D ∨ C ∈ int_triangle D A B

  proof
    ¬(A = B) ∧ ¬(D = A) ∧ ¬(A = C) ∧ ¬(B = D) ∧ ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B     [TetraABCD] by H1, Tetralateral_DEF;
    consider a d such that
    Line a ∧ A ∈ a ∧ B ∈ a  ∧
    Line d ∧ D ∈ d ∧ A ∈ d     [ad_line] by TetraABCD, I1;
    consider l m such that
    Line l ∧ A ∈ l ∧ C ∈ l  ∧
    Line m ∧ B ∈ m ∧ D ∈ m     [lm_line] by TetraABCD, I1;
    C ∉ a ∧ C ∉ d ∧ B ∉ l ∧ D ∉ l ∧ A ∉ m ∧ C ∉ m ∧ ¬Collinear A B D ∧ ¬Collinear B D A          [tetra'] by TetraABCD, ad_line, lm_line, Collinear_DEF, ∉, CollinearSymmetry;
    ¬(B,D same_side l)     [Bsim_lD] by CintDAB, lm_line, InteriorOpposite, -, SameSideSymmetric;
    cases;
    suppose ¬(A,C same_side m);
    qed     by lm_line, H1, Bsim_lD, -, DoubleNotSimImpliesDiagonalsIntersect;
    suppose A,C same_side m;
      C,A same_side m     [Csim_mA] by lm_line, -, tetra', SameSideSymmetric;
      C,B same_side d  ∧  C,D same_side a     by ad_line, CintDAB, InteriorUse;
      C ∈ int_angle A B D  ∧  C ∈ int_angle B D A     by tetra', ad_line, lm_line, Csim_mA, -, IN_InteriorAngle;
      C ∈ int_triangle D A B     by CintDAB, -, IN_InteriorTriangle;
    qed     by -;
  end;
`;;

let InteriorTriangleSymmetry = thm `;
  ∀ A B C P. P ∈ int_triangle A B C  ⇒ P ∈ int_triangle B C A
  by IN_InteriorTriangle;
`;;

let FourChoicesTetralateral = thm `;
  let A B C D be point;
  let a be point_set;
  assume Tetralateral A B C D                   [H1];
  assume Line a ∧ A ∈ a ∧ B ∈ a                 [a_line];
  assume C,D same_side a                        [Csim_aD];
  thus ConvexQuadrilateral A B C D  ∨  ConvexQuadrilateral A B D C  ∨
       D ∈ int_triangle A B C  ∨  C ∈ int_triangle D A B

  proof
     ¬(A = B) ∧ ¬Collinear A B C ∧ ¬Collinear C D A ∧ ¬Collinear D A B ∧ Tetralateral A B D C     [TetraABCD] by H1, Tetralateral_DEF, TetralateralSymmetry;
    ¬Collinear C A D ∧ C ∉ a ∧ D ∉ a     [notCDa] by TetraABCD, CollinearSymmetry, a_line, Collinear_DEF, ∉;
    C ∈ int_angle D A B  ∨  D ∈ int_angle C A B     by TetraABCD, a_line, -, Csim_aD, AngleOrdering;
    cases     by -;
    suppose C ∈ int_angle D A B;
      ConvexQuadrilateral A B C D  ∨  C ∈ int_triangle D A B     by H1, -, FourChoicesTetralateralHelp;
    qed     by -;
    suppose D ∈ int_angle C A B;
      ConvexQuadrilateral A B D C  ∨  D ∈ int_triangle C A B     by TetraABCD, -, FourChoicesTetralateralHelp;
    qed     by -, InteriorTriangleSymmetry;
  end;
`;;

let QuadrilateralSymmetry = thm `;
  ∀ A B C D:point. Quadrilateral A B C D  ⇒
  Quadrilateral B C D A  ∧  Quadrilateral C D A B  ∧  Quadrilateral D A B C
  by Quadrilateral_DEF, INTER_COMM, TetralateralSymmetry, Quadrilateral_DEF;
`;;

let FiveChoicesQuadrilateral = thm `;
  let A B C D be point;
  let l m be point_set;
  assume Quadrilateral A B C D                                                  [H1];
  assume Line l ∧ A ∈ l ∧ C ∈ l  ∧  Line m ∧ B ∈ m ∧ D ∈ m                                              [lm_line];
  thus (ConvexQuadrilateral A B C D  ∨  A ∈ int_triangle B C D  ∨
  B ∈ int_triangle C D A  ∨  C ∈ int_triangle D A B  ∨  D ∈ int_triangle A B C)  ∧
  (¬(B,D same_side l) ∨ ¬(A,C same_side m))

  proof
    Tetralateral A B C D     [H1Tetra] by H1, Quadrilateral_DEF;
    ¬(A = B) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(C = D)     [Distinct] by H1Tetra, Tetralateral_DEF;
    consider a c such that
    Line a ∧ A ∈ a ∧ B ∈ a  ∧
    Line c ∧ C ∈ c ∧ D ∈ c     [ac_line] by Distinct, I1;
    Quadrilateral C D A B  ∧  Tetralateral C D A B     [tetraCDAB] by H1, QuadrilateralSymmetry, Quadrilateral_DEF;
    ¬ConvexQuadrilateral A B D C  ∧  ¬ConvexQuadrilateral C D B A     [notconvquad] by Distinct, I1, H1, -, ConvexQuadImpliesDiagonalsIntersect;
    ConvexQuadrilateral A B C D  ∨  A ∈ int_triangle B C D  ∨
    B ∈ int_triangle C D A  ∨  C ∈ int_triangle D A B  ∨  D ∈ int_triangle A B C     [5choices]
    proof
      A,B same_side c  ∨  C,D same_side a     by H1, ac_line, SegmentSameSideOppositeLine;
      cases     by -;
      suppose C,D same_side a;
      qed     by H1Tetra, ac_line, -, notconvquad, FourChoicesTetralateral;
      suppose A,B same_side c;
        ConvexQuadrilateral C D A B  ∨  B ∈ int_triangle C D A  ∨  A ∈ int_triangle B C D     [X1] by tetraCDAB, ac_line, -, notconvquad, FourChoicesTetralateral;
      qed     by -, QuadrilateralSymmetry, ConvexQuad_DEF;
    end;
    ¬(B,D same_side l) ∨ ¬(A,C same_side m)     by -, lm_line, ConvexQuadImpliesDiagonalsIntersect, IN_InteriorTriangle, InteriorAngleSymmetry, InteriorOpposite;
  qed     by 5choices, -;
`;;

let IntervalSymmetry = thm `;
  ∀ A B: point. open (A,B) = open (B,A)
  by B1', EXTENSION;
`;;

let SegmentSymmetry = thm `;
  ∀ A B: point. seg A B = seg B A
  by Segment_DEF, IntervalSymmetry, SET_RULE;
`;;

let C1OppositeRay = thm `;
  let O P be point;
  let s be point_set;
  assume Segment s ∧ ¬(O = P)                   [H1];
  thus ∃ Q. P ∈ open (O,Q)  ∧  seg P Q ≡ s

  proof
    consider Z such that
    P ∈ open (O,Z)  ∧  ¬(P = Z)     [OPZ] by H1, B2', B1';
    consider Q such that
    Q ∈ ray P Z ━ P ∧ seg P Q ≡ s     [PQeq] by H1, -, C1;
    P ∈ open (Q,O)     by OPZ, -, OppositeRaysIntersect1pointHelp;
  qed     by -, B1', PQeq;
`;;

let OrderedCongruentSegments = thm `;
  let A B C D F be point;
  assume ¬(A = C) ∧ ¬(D = F)                            [H1];
  assume seg A C ≡ seg D F                              [H2];
  assume B ∈ open (A,C)                                 [H3];
  thus ∃ E. E ∈ open (D,F)  ∧  seg A B ≡ seg D E

  proof
    Segment (seg A B) ∧ Segment (seg A C) ∧ Segment (seg B C) ∧ Segment (seg D F)     [segs] by H3, B1', H1, SEGMENT;
    seg D F ≡ seg A C     [DFeqAC] by -, H2, C2Symmetric;
    consider E such that
    E ∈ ray D F ━ D ∧ seg D E ≡ seg A B     [DEeqAB] by segs, H1, C1;
    ¬(E = D) ∧ Collinear D E F ∧ D ∉ open (F,E)     [ErDF] by -, IN_DELETE, IN_Ray, B1', CollinearSymmetry, ∉;
    consider F' such that
    E ∈ open (D,F') ∧ seg E F' ≡ seg B C     [DEF'] by segs, -, C1OppositeRay;
    seg D F' ≡ seg A C     [DF'eqAC] by DEF', H3, DEeqAB, C3;
    Segment (seg D F') ∧ Segment (seg D E)     by DEF', B1', SEGMENT;
    seg A C ≡ seg D F' ∧ seg A B ≡ seg D E     [ABeqDE] by segs, -, DF'eqAC, C2Symmetric, DEeqAB;
    F' ∈ ray D E ━ D  ∧  F ∈ ray D E ━ D     by DEF', IntervalRayEZ, ErDF, IN_Ray, H1, IN_DELETE;
    F' = F     by ErDF, segs, -, DF'eqAC, DFeqAC, C1;
  qed     by -, DEF', ABeqDE;
`;;

let SegmentSubtraction = thm `;
  let A B C A' B' C' be point;
  assume B ∈ open (A,C)  ∧  B' ∈ open (A',C')           [H1];
  assume seg A B ≡ seg A' B'                            [H2];
  assume seg A C ≡ seg A' C'                            [H3];
  thus seg B C ≡ seg B' C'

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ Collinear A B C ∧ Segment (seg A' C') ∧ Segment (seg B' C')     [Distinct] by H1, B1', SEGMENT;
    consider Q such that
    B ∈ open (A,Q)  ∧  seg B Q ≡ seg B' C'     [defQ] by -, C1OppositeRay;
    seg A Q ≡ seg A' C'     [AQ_A'C'] by H1, H2, -, C3;
    ¬(A = Q)  ∧  Collinear A B Q  ∧  A ∉ open (C,B)  ∧  A ∉ open (Q,B)     by defQ, B1', H1, B3', ∉;
    C ∈ ray A B ━ A  ∧  Q ∈ ray A B ━ A     by Distinct, -, IN_Ray, IN_DELETE;
    C = Q     by Distinct, -, AQ_A'C', H3, C1;
  qed     by defQ, -;
`;;

let SegmentOrderingUse = thm `;
  let A B be point;
  let s be point_set;
  assume Segment s  ∧  ¬(A = B)                 [H1];
  assume s <__ seg A B                          [H2];
  thus ∃ G. G ∈ open (A,B)  ∧  s ≡ seg A G

  proof
    consider A' B' G' such that
    seg A B = seg A' B'  ∧  G' ∈ open (A',B')  ∧  s ≡ seg A' G'     [H2'] by H2, SegmentOrdering_DEF;
    ¬(A' = G') ∧ ¬(A' = B')  ∧  seg A' B' ≡ seg A B     [A'notB'G'] by -, B1', H1, SEGMENT, C2Reflexive;
    consider G such that
    G ∈ open (A,B)  ∧  seg A' G' ≡ seg A G     [AGB] by A'notB'G', H1, H2', -,  OrderedCongruentSegments;
    s ≡ seg A G     by H1, A'notB'G', -, B1', SEGMENT, H2', C2Transitive;
  qed     by AGB, -;
`;;

let SegmentTrichotomy1 = thm `;
  let s t be point_set;
  assume s <__ t                        [H1];
  thus ¬(s ≡ t)

  proof
    consider A B G such that
    Segment s ∧ t = seg A B ∧ G ∈ open (A,B) ∧ s ≡ seg A G     [H1'] by H1, SegmentOrdering_DEF;
    ¬(A = G) ∧ ¬(A = B) ∧ ¬(G = B)     [Distinct] by H1', B1';
    seg A B ≡ seg A B     [ABrefl] by -, SEGMENT, C2Reflexive;
    G ∈ ray A B ━ A  ∧  B ∈ ray A B ━ A     by H1', IntervalRay, EndpointInRay, Distinct, IN_DELETE;
    ¬(seg A G ≡ seg A B)  ∧ seg A G ≡ s     by Distinct, SEGMENT, -, ABrefl, C1, H1', C2Symmetric;
  qed     by Distinct, H1', SEGMENT, -, C2Transitive;
`;;

let SegmentTrichotomy2 = thm `;
  let s t u be point_set;
  assume s <__ t                                [H1];
  assume Segment u  ∧  t ≡ u                    [H2];
  thus s <__ u

  proof
    consider A B P such that
    Segment s  ∧  t = seg A B  ∧  P ∈ open (A,B)  ∧  s ≡ seg A P     [H1'] by H1, SegmentOrdering_DEF;
    ¬(A = B) ∧ ¬(A = P)     [Distinct] by -, B1';
    consider X Y such that
    u = seg X Y ∧ ¬(X = Y)     [uXY] by H2, SEGMENT;
    consider Q such that
    Q ∈ open (X,Y)  ∧  seg A P ≡ seg X Q     [XQY] by Distinct, -, H1', H2, OrderedCongruentSegments;
    ¬(X = Q)  ∧  s ≡ seg X Q     by -, B1', H1', Distinct, SEGMENT, XQY, C2Transitive;
  qed     by H1', uXY, XQY, -, SegmentOrdering_DEF;
`;;

let SegmentOrderTransitivity = thm `;
  let s t u be point_set;
  assume s <__ t  ∧  t <__ u            [H1];
  thus s <__ u

  proof
    consider A B G such that
    u = seg A B  ∧  G ∈ open (A,B)  ∧  t ≡ seg A G     [H1'] by H1, SegmentOrdering_DEF;
    ¬(A = B) ∧ ¬(A = G) ∧ Segment s     [Distinct] by H1',  B1', H1, SegmentOrdering_DEF;
    s <__ seg A G     by H1, H1', Distinct, SEGMENT, SegmentTrichotomy2;
    consider F such that
    F ∈ open (A,G) ∧ s ≡ seg A F     [AFG] by Distinct, -, SegmentOrderingUse;
    F ∈ open (A,B)     by H1', IntervalsAreConvex, -, SUBSET;
  qed     by Distinct, H1', -, AFG, SegmentOrdering_DEF;
`;;

let SegmentTrichotomy = thm `;
  let s t be point_set;
  assume Segment s ∧ Segment t                          [H1];
  thus (s ≡ t  ∨  s <__ t  ∨  t <__ s)  ∧  ¬(s ≡ t ∧ s <__ t)  ∧
       ¬(s ≡ t ∧ t <__ s)  ∧  ¬(s <__ t ∧ t <__ s)

  proof
    ¬(s ≡ t  ∧  s <__ t)     [Not12]
    proof
      assume s <__ t;
    qed by -, SegmentTrichotomy1;
    ¬(s ≡ t  ∧  t <__ s)     [Not13]
    proof
      assume t <__ s;
      ¬(t ≡ s) by -, SegmentTrichotomy1;
    qed by H1, -, C2Symmetric;
    ¬(s <__ t  ∧  t <__ s)     [Not23]
    proof
      assume s <__ t  ∧  t <__ s;
      s <__ s     by H1, -, SegmentOrderTransitivity;
    qed     by -, SegmentTrichotomy1, H1, C2Reflexive;
    consider O P such that
    s = seg O P  ∧  ¬(O = P)     [sOP] by H1, SEGMENT;
    consider Q such that
    Q ∈ ray O P ━ O  ∧  seg O Q ≡ t     [QrOP] by H1, -, C1;
    O ∉ open (Q,P)  ∧  Collinear O P Q   ∧  ¬(O = Q)     [notQOP] by -, IN_DELETE, IN_Ray;
    s ≡ seg O P  ∧  t ≡ seg O Q  ∧  seg O Q ≡ t  ∧  seg O P ≡ s     [stOPQ] by H1, sOP, -, SEGMENT, QrOP, C2Reflexive, C2Symmetric;
    cases;
    suppose Q = P;
      s ≡ t     by -, sOP, QrOP;
    qed     by -, Not12, Not13, Not23;
    suppose ¬(Q = P);
      P ∈ open (O,Q)  ∨  Q ∈ open (O,P)     by sOP, -, notQOP, B3', B1', ∉;
      s <__ seg O Q  ∨  t <__ seg O P     by H1, -, stOPQ, SegmentOrdering_DEF;
      s <__ t  ∨  t <__ s     by -, H1, stOPQ, SegmentTrichotomy2;
    qed     by -, Not12, Not13, Not23;
  end;
`;;

let C4Uniqueness = thm `;
  let O A B P be point;
  let l be point_set;
  assume Line l ∧ O ∈ l ∧ A ∈ l ∧ ¬(O = A)     [H1];
  assume B ∉ l ∧ P ∉ l ∧ P,B same_side l       [H2];
  assume ∡ A O P ≡ ∡ A O B             [H3];
  thus ray O B = ray O P

  proof
    ¬(O = B) ∧ ¬(O = P) ∧ Ray (ray O B) ∧ Ray (ray O P)     [Distinct] by H2, H1, ∉, RAY;
    ¬Collinear A O B  ∧  B,B same_side l     [Bsim_lB] by H1, H2, I1, Collinear_DEF, ∉, SameSideReflexive;
    Angle (∡ A O B)  ∧  ∡ A O B ≡ ∡ A O B     by -, ANGLE, C5Reflexive;
  qed     by -, H1, H2, Distinct, Bsim_lB, H3, C4;
`;;

let AngleSymmetry = thm `;
  ∀ A O B. ∡ A O B = ∡ B O A
  by Angle_DEF, UNION_COMM;
`;;

let TriangleCongSymmetry = thm `;
  let A B C A' B' C' be point;
  assume A,B,C ≅ A',B',C'                                       [H1];
  thus A,C,B ≅ A',C',B' ∧ B,A,C ≅ B',A',C' ∧
       B,C,A ≅ B',C',A' ∧ C,A,B ≅ C',A',B' ∧ C,B,A ≅ C',B',A'

  proof
    ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
    seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧ seg B C ≡ seg B' C' ∧
    ∡ A B C ≡ ∡ A' B' C' ∧ ∡ B C A ≡ ∡ B' C' A' ∧ ∡ C A B ≡ ∡ C' A' B'    [H1'] by H1, TriangleCong_DEF;
    seg B A ≡ seg B' A' ∧ seg C A ≡ seg C' A' ∧ seg C B ≡ seg C' B'     [segments] by H1', SegmentSymmetry;
    ∡ C B A ≡ ∡ C' B' A' ∧ ∡ A C B ≡ ∡ A' C' B' ∧ ∡ B A C ≡ ∡ B' A' C'     by H1', AngleSymmetry;
  qed by CollinearSymmetry, H1', segments, -, TriangleCong_DEF;
`;;

let SAS = thm `;
  let A B C A' B' C' be point;
  assume ¬Collinear A B C ∧ ¬Collinear A' B' C'         [H1];
  assume seg B A ≡ seg B' A'  ∧  seg B C ≡ seg B' C'            [H2];
  assume ∡ A B C ≡ ∡ A' B' C'                           [H3];
  thus A,B,C ≅ A',B',C'

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(A' = C')     [Distinct] by H1, NonCollinearImpliesDistinct; :: 134
    consider c such that
    Line c ∧ A ∈ c ∧ B ∈ c     [c_line] by Distinct, I1;
    C ∉ c     [notCc] by H1, c_line, Collinear_DEF, ∉;
    ∡ B C A ≡ ∡ B' C' A'     [BCAeq] by H1, H2, H3, C6;
    ∡ B A C ≡ ∡ B' A' C'     [BACeq] by H1, CollinearSymmetry, H2, H3, AngleSymmetry, C6;
    consider Y such that
    Y ∈ ray A C ━ A  ∧  seg A Y ≡ seg A' C'     [YrAC] by Distinct, SEGMENT, C1;
    Y ∉ c  ∧  Y,C same_side c     [Ysim_cC] by c_line, notCc, -, RaySameSide;
    ¬Collinear Y A B     [YABncol] by c_line, -, Distinct, I1, Collinear_DEF, ∉;
    ray A Y = ray A C  ∧  ∡ Y A B = ∡ C A B     by Distinct, YrAC, RayWellDefined, Angle_DEF;
    ∡ Y A B ≡ ∡ C' A' B'     by BACeq, -, AngleSymmetry;
    ∡ A B Y ≡ ∡ A' B' C'     [ABYeq] by YABncol, H1, CollinearSymmetry, H2, SegmentSymmetry, YrAC, -, C6;
    Angle (∡ A B C) ∧ Angle (∡ A' B' C') ∧ Angle (∡ A B Y)     by H1, CollinearSymmetry, YABncol, ANGLE;
    ∡ A B Y ≡ ∡ A B C     [ABYeqABC] by -, ABYeq, -, H3, C5Symmetric, C5Transitive;
    ray B C = ray B Y  ∧  ¬(Y = B)  ∧  Y ∈ ray B C     by c_line, Distinct, notCc, Ysim_cC, ABYeqABC, C4Uniqueness, ∉, -, EndpointInRay;
    Collinear B C Y  ∧  Collinear A C Y     by -, YrAC, IN_DELETE, IN_Ray;
    C = Y     by -, I1, Collinear_DEF, H1;
    seg A C ≡ seg A' C'     by -, YrAC;
  qed     by H1, H2, SegmentSymmetry, -, H3, BCAeq, BACeq, AngleSymmetry, TriangleCong_DEF;
`;;

let ASA = thm `;
  let A B C A' B' C' be point;
  assume ¬Collinear A B C ∧ ¬Collinear A' B' C'         [H1];
  assume seg A C ≡ seg A' C'                                    [H2];
  assume ∡ C A B ≡ ∡ C' A' B'  ∧  ∡ B C A ≡ ∡ B' C' A'          [H3];
  thus A,B,C ≅ A',B',C'

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬(A' = B') ∧ ¬(A' = C') ∧ ¬(B' = C') ∧ Segment (seg C' B')     [Distinct] by H1, NonCollinearImpliesDistinct, SEGMENT;
    consider D such that
    D ∈ ray C B ━ C  ∧  seg C D ≡ seg C' B'  ∧  ¬(D = C)     [DrCB] by -, C1, IN_DELETE;
    Collinear C B D     [CBDcol] by -, IN_DELETE, IN_Ray;
    ¬Collinear D C A ∧ Angle (∡ C A D) ∧ Angle (∡ C' A' B') ∧ Angle (∡ C A B)     [DCAncol] by H1, CollinearSymmetry, -, DrCB, NoncollinearityExtendsToLine, H1, ANGLE;
    consider b such that
    Line b ∧ A ∈ b ∧ C ∈ b     [b_line] by Distinct, I1;
    B ∉ b ∧ ¬(D = A)     [notBb] by H1, -, Collinear_DEF, ∉, DCAncol, NonCollinearImpliesDistinct;
    D ∉ b  ∧  D,B same_side b     [Dsim_bB] by b_line, -, DrCB, RaySameSide;
    ray C D = ray C B     by Distinct, DrCB, RayWellDefined;
    ∡ D C A ≡ ∡ B' C' A'     by H3, -, Angle_DEF;
    D,C,A ≅ B',C',A'     by DCAncol, H1, CollinearSymmetry, DrCB, H2, SegmentSymmetry, -, SAS;
    ∡ C A D ≡ ∡ C' A' B'     by -, TriangleCong_DEF;
    ∡ C A D ≡ ∡ C A B     by DCAncol, -, H3, C5Symmetric, C5Transitive;
    ray A B = ray A D  ∧  D ∈ ray A B     by b_line, Distinct, notBb, Dsim_bB, -, C4Uniqueness, notBb, EndpointInRay;
    Collinear A B D     by -, IN_Ray;
    D = B     by I1, -, Collinear_DEF, CBDcol, H1;
    seg C B ≡ seg C' B'     by -, DrCB;
    B,C,A ≅ B',C',A'     by H1, CollinearSymmetry, -, H2, SegmentSymmetry, H3, SAS;
  qed     by -, TriangleCongSymmetry;
`;;

let AngleSubtraction = thm `;
  let A O B A' O' B' G G' be point;
  assume G ∈ int_angle A O B  ∧  G' ∈ int_angle A' O' B'        [H1];
  assume ∡ A O B ≡ ∡ A' O' B'  ∧  ∡ A O G ≡ ∡ A' O' G'  [H2];
  thus ∡ G O B ≡ ∡ G' O' B'

  proof
    ¬Collinear A O B ∧ ¬Collinear A' O' B'     [A'O'B'ncol] by H1, IN_InteriorAngle;
    ¬(A = O) ∧ ¬(O = B) ∧ ¬(G = O) ∧ ¬(G' = O') ∧ Segment (seg O' A') ∧ Segment (seg O' B')     [Distinct] by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp, SEGMENT;
   consider X Y such that
   X ∈ ray O A ━ O  ∧  seg O X ≡ seg O' A'  ∧  Y ∈ ray O B ━ O  ∧  seg O Y ≡ seg O' B'     [XYexists] by -, C1;
    G ∈ int_angle X O Y     [GintXOY] by H1, XYexists, InteriorWellDefined, InteriorAngleSymmetry;
    consider H H' such that
    H ∈ open (X,Y)  ∧  H ∈ ray O G ━ O  ∧
    H' ∈ open (A',B')  ∧  H' ∈ ray O' G' ━ O'     [Hexists] by -, H1, Crossbar_THM;
    H ∈ int_angle X O Y  ∧  H' ∈ int_angle A' O' B'     [HintXOY] by GintXOY, H1, -, WholeRayInterior;
    ray O X = ray O A  ∧  ray O Y = ray O B  ∧  ray O H = ray O G  ∧  ray O' H' = ray O' G'     [Orays] by Distinct, XYexists, Hexists, RayWellDefined;
    ∡ X O Y ≡ ∡ A' O' B'  ∧  ∡ X O H ≡ ∡ A' O' H'     [H2'] by H2, -, Angle_DEF;
    ¬Collinear X O Y     by GintXOY, IN_InteriorAngle;
    X,O,Y ≅ A',O',B'     by -, A'O'B'ncol, H2', XYexists, SAS;
    seg X Y ≡ seg A' B'  ∧  ∡ O Y X ≡ ∡ O' B' A'  ∧  ∡ Y X O ≡ ∡ B' A' O'     [XOYcong] by -, TriangleCong_DEF;
    ¬Collinear O H X ∧ ¬Collinear O' H' A' ∧ ¬Collinear O Y H ∧ ¬Collinear O' B' H'     [OHXncol] by HintXOY, InteriorEZHelp, InteriorAngleSymmetry, CollinearSymmetry;
    ray X H = ray X Y  ∧  ray A' H' = ray A' B'  ∧  ray Y H = ray Y X  ∧  ray B' H' = ray B' A'     [Hrays] by Hexists, B1', IntervalRay;
    ∡ H X O ≡ ∡ H' A' O'     by XOYcong, -, Angle_DEF;
    O,H,X ≅ O',H',A'     by OHXncol, XYexists, -, H2', ASA;
    seg X H ≡ seg A' H'     by -, TriangleCong_DEF, SegmentSymmetry;
    seg H Y ≡ seg H' B'     by Hexists, XOYcong, -, SegmentSubtraction;
    seg Y O  ≡ seg B' O'  ∧  seg Y H ≡ seg B' H'     [YHeq] by XYexists, -, SegmentSymmetry;
    ∡ O Y H ≡ ∡ O' B' H'     by XOYcong, Hrays, Angle_DEF;
    O,Y,H ≅ O',B',H'     by OHXncol, YHeq, -, SAS;
  ∡ H O Y ≡ ∡ H' O' B'     by -, TriangleCong_DEF;
  qed     by -, Orays, Angle_DEF;
`;;

let OrderedCongruentAngles = thm `;
  let A O B A' O' B' G be point;
  assume ¬Collinear A' O' B'                                    [H1];
  assume ∡ A O B ≡ ∡ A' O' B'                           [H2];
  assume G ∈ int_angle A O B                                    [H3];
  thus ∃ G'. G' ∈ int_angle A' O' B'  ∧  ∡ A O G ≡ ∡ A' O' G'

  proof
    ¬Collinear A O B     [AOBncol] by H3, IN_InteriorAngle;
    ¬(A = O) ∧ ¬(O = B) ∧ ¬(A' = B') ∧ ¬(O = G) ∧ Segment (seg O' A') ∧ Segment (seg O' B')     [Distinct] by AOBncol, H1, NonCollinearImpliesDistinct, H3, InteriorEZHelp, SEGMENT;
    consider X Y such that
    X ∈ ray O A ━ O  ∧  seg O X ≡ seg O' A'  ∧  Y ∈ ray O B ━ O  ∧  seg O Y ≡ seg O' B'     [defXY] by -, C1;
    G ∈ int_angle X O Y     [GintXOY] by H3, -, InteriorWellDefined, InteriorAngleSymmetry;
    ¬Collinear X O Y ∧ ¬(X = Y)     [XOYncol] by -, IN_InteriorAngle, NonCollinearImpliesDistinct;
    consider H such that
    H ∈ open (X,Y)  ∧  H ∈ ray O G ━ O     [defH] by GintXOY, Crossbar_THM;
    ray O X = ray O A  ∧  ray O Y = ray O B  ∧  ray O H = ray O G     [Orays] by Distinct, defXY, -, RayWellDefined;
    ∡ X O Y ≡ ∡ A' O' B'     by H2, -, Angle_DEF;
    X,O,Y ≅ A',O',B'     by XOYncol, H1, defXY, -, SAS;
    seg X Y ≡ seg A' B'  ∧  ∡ O X Y ≡ ∡ O' A' B'     [YXOcong] by -, TriangleCong_DEF, AngleSymmetry;
    consider G' such that
    G' ∈ open (A',B')  ∧  seg X H ≡ seg A' G'     [A'G'B'] by XOYncol, Distinct, -, defH, OrderedCongruentSegments;
    G' ∈ int_angle A' O' B'     [G'intA'O'B'] by H1, -, ConverseCrossbar;
    ray X H = ray X Y  ∧  ray A' G' = ray A' B'     by defH, A'G'B', IntervalRay;
    ∡ O X H ≡ ∡ O' A' G'     [HXOeq] by -, Angle_DEF, YXOcong;
    H ∈ int_angle X O Y     by GintXOY, defH, WholeRayInterior;
    ¬Collinear O X H ∧ ¬Collinear O' A' G'     by -, G'intA'O'B', InteriorEZHelp, CollinearSymmetry;
    O,X,H ≅ O',A',G'     by -, A'G'B', defXY, SegmentSymmetry, HXOeq, SAS;
    ∡ X O H ≡ ∡ A' O' G'     by -, TriangleCong_DEF, AngleSymmetry;
    ∡ A O G ≡ ∡ A' O' G'     by -, Orays, Angle_DEF;
  qed     by G'intA'O'B', -;
`;;

let AngleAddition = thm `;
  let A O B A' O' B' G G' be point;
  assume G ∈ int_angle A O B  ∧  G' ∈ int_angle A' O' B'                [H1];
  assume ∡ A O G ≡ ∡ A' O' G'  ∧  ∡ G O B ≡ ∡ G' O' B'          [H2];
  thus ∡ A O B ≡ ∡ A' O' B'

  proof
    ¬Collinear A O B ∧ ¬Collinear A' O' B'     [AOBncol] by H1, IN_InteriorAngle;
    ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B) ∧ ¬(A' = O') ∧ ¬(A' = B') ∧ ¬(O' = B') ∧ ¬(G = O)     [Distinct] by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp;
    consider a b such that
    Line a ∧ O ∈ a ∧ A ∈ a  ∧
    Line b ∧ O ∈ b ∧ B ∈ b     [a_line] by Distinct, I1;
    consider g such that
    Line g ∧ O ∈ g ∧ G ∈ g     [g_line] by  Distinct, I1;
    G ∉ a ∧ G,B same_side a     [H1'] by a_line, H1, InteriorUse;
    ¬Collinear A O G ∧ ¬Collinear A' O' G'     [AOGncol] by H1, InteriorEZHelp, IN_InteriorAngle;
    Angle (∡ A O B) ∧ Angle (∡ A' O' B') ∧ Angle (∡ A O G) ∧ Angle (∡ A' O' G')     [angles] by AOBncol, -, ANGLE;
    ∃! r. Ray r ∧ ∃ X. ¬(O = X) ∧ r = ray O X ∧ X ∉ a ∧ X,G same_side a ∧ ∡ A O X ≡ ∡ A' O' B'     by -, Distinct, a_line, H1', C4;
    consider X such that
    X ∉ a ∧ X,G same_side a ∧ ∡ A O X ≡ ∡ A' O' B'     [Xexists] by -;
    ¬Collinear A O X     [AOXncol] by -, a_line, Distinct, I1, Collinear_DEF, ∉;
    ∡ A' O' B' ≡ ∡ A O X     by -, AOBncol, ANGLE, Xexists, C5Symmetric;
    consider Y such that
    Y ∈ int_angle A O X  ∧  ∡ A' O' G' ≡ ∡ A O Y     [YintAOX] by AOXncol, -, H1, OrderedCongruentAngles;
    ¬Collinear A O Y     by -, InteriorEZHelp;
    ∡ A O Y  ≡ ∡ A O G     [AOGeq] by -, angles, -, ANGLE, YintAOX, H2, C5Transitive, C5Symmetric;
    consider x such that
    Line x ∧ O ∈ x ∧ X ∈ x     by Distinct, I1;
    Y ∉ a ∧ Y,X same_side a     by a_line, -, YintAOX, InteriorUse;
    Y ∉ a ∧ Y,G same_side a     by  a_line, -, Xexists, H1', SameSideTransitive;
    ray O G = ray O Y     by a_line, Distinct, H1', -, AOGeq, C4Uniqueness;
    G ∈ ray O Y ━ O     by Distinct, -, EndpointInRay, IN_DELETE;
    G ∈ int_angle A O X     [GintAOX] by YintAOX, -, WholeRayInterior;
    ∡ G O X ≡ ∡ G' O' B'     [GOXeq] by -, H1, Xexists, H2, AngleSubtraction;
    ¬Collinear G O X ∧ ¬Collinear G O B ∧ ¬Collinear G' O' B'     [GOXncol] by GintAOX, H1, InteriorAngleSymmetry, InteriorEZHelp, CollinearSymmetry;
    Angle (∡ G O X) ∧ Angle (∡ G O B) ∧ Angle (∡ G' O' B')     by -, ANGLE;
    ∡ G O X ≡ ∡ G O B     [G'O'Xeq] by  angles, -, GOXeq, C5Symmetric, H2, C5Transitive;
    ¬(A,X same_side g) ∧ ¬(A,B same_side g)     [Ansim_aXB] by g_line, GintAOX, H1, InteriorOpposite;
    A ∉ g ∧ B ∉ g ∧ X ∉ g     [notABXg] by g_line, AOGncol, GOXncol, Distinct, I1, Collinear_DEF, ∉;
    X,B same_side g     by g_line, -, Ansim_aXB, AtMost2Sides;
    ray O X = ray O B     by g_line, Distinct, notABXg, -, G'O'Xeq, C4Uniqueness;
  qed     by -, Xexists, Angle_DEF;
`;;

let AngleOrderingUse = thm `;
  let A O B be point;
  let α be point_set;
  assume Angle α  ∧  ¬Collinear A O B                   [H1];
  assume α <_ang ∡ A O B                                [H3];
  thus ∃ G. G ∈ int_angle A O B ∧ α ≡ ∡ A O G

  proof
    consider A' O' B' G' such that
    ¬Collinear A' O' B'  ∧  ∡ A O B = ∡ A' O' B'  ∧  G' ∈ int_angle A' O' B'  ∧  α ≡ ∡ A' O' G'     [H3'] by H3, AngleOrdering_DEF;
    Angle (∡ A O B) ∧ Angle (∡ A' O' B') ∧ Angle (∡ A' O' G')     [angles] by H1, -, ANGLE, InteriorEZHelp;
    ∡ A' O' B' ≡ ∡ A O B     by -, H3', C5Reflexive;
    consider G such that
    G ∈ int_angle A O B  ∧  ∡ A' O' G' ≡ ∡ A O G     [GintAOB] by H1, H3', -,  OrderedCongruentAngles;
    α ≡ ∡ A O G     by H1, angles, -, InteriorEZHelp, ANGLE, H3', GintAOB, C5Transitive;
  qed     by -, GintAOB;
`;;

let AngleTrichotomy1 = thm `;
  let α β be point_set;
  assume α <_ang β              [H1];
  thus ¬(α ≡ β)

  proof
    assume α ≡ β [Con];
    consider A O B G such that
    Angle α ∧ ¬Collinear A O B ∧ β = ∡ A O B ∧ G ∈ int_angle A O B ∧ α ≡ ∡ A O G     [H1'] by H1, AngleOrdering_DEF;
    ¬(A = O) ∧ ¬(O = B) ∧ ¬Collinear A O G     [Distinct] by H1', NonCollinearImpliesDistinct, InteriorEZHelp;
    consider a such that
    Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by Distinct, I1;
    consider b such that
    Line b ∧ O ∈ b ∧ B ∈ b     [b_line] by Distinct, I1;
    B ∉ a     [notBa] by a_line, H1', Collinear_DEF, ∉;
    G ∉ a ∧ G ∉ b ∧ G,B same_side a     [GintAOB] by a_line, b_line, H1', InteriorUse;
    ∡ A O G ≡ α     by H1', Distinct, ANGLE, C5Symmetric;
    ∡ A O G ≡ ∡ A O B     by H1', Distinct, ANGLE, -, Con, C5Transitive;
    ray O B = ray O G     by a_line, Distinct, notBa, GintAOB, -, C4Uniqueness;
    G ∈ b     by Distinct, -, EndpointInRay, b_line, RayLine, SUBSET;
  qed     by -, GintAOB, ∉;
`;;

let AngleTrichotomy2 = thm `;
  let α β γ be point_set;
  assume α <_ang β              [H1];
  assume Angle γ                [H2];
  assume β ≡ γ                  [H3];
  thus α <_ang γ

  proof
    consider A O B G such that
    Angle α ∧ ¬Collinear A O B ∧ β = ∡ A O B ∧ G ∈ int_angle A O B ∧ α ≡ ∡ A O G     [H1'] by H1, AngleOrdering_DEF;
    consider A' O' B' such that
    γ = ∡ A' O' B' ∧ ¬Collinear A' O' B'     [γA'O'B'] by H2, ANGLE;
    consider G' such that
    G' ∈ int_angle A' O' B' ∧ ∡ A O G ≡ ∡ A' O' G'     [G'intA'O'B'] by γA'O'B', H1', H3,  OrderedCongruentAngles;
    ¬Collinear A O G ∧ ¬Collinear A' O' G'     [ncol] by H1', -, InteriorEZHelp;
    α ≡ ∡ A' O' G'     by H1', ANGLE, -, G'intA'O'B', C5Transitive;
  qed     by H1', -, ncol, γA'O'B', G'intA'O'B', -, AngleOrdering_DEF;
`;;

let AngleOrderTransitivity = thm `;
  let α β γ be point_set;
    assume α <_ang β [H0];
    assume β <_ang γ [H2];
    thus α <_ang γ

  proof
    consider A O B G such that
    Angle β ∧ ¬Collinear A O B ∧ γ = ∡ A O B ∧ G ∈ int_angle A O B ∧ β ≡ ∡ A O G     [H2'] by H2, AngleOrdering_DEF;
    ¬Collinear A O G     [AOGncol] by H2',  InteriorEZHelp;
    Angle α ∧ Angle (∡ A O G)  ∧ Angle γ     [angles] by H0, AngleOrdering_DEF, H2', -, ANGLE;
    α <_ang ∡ A O G     by H0, H2', -, AngleTrichotomy2;
    consider F such that
    F ∈ int_angle A O G ∧ α ≡ ∡ A O F     [FintAOG] by angles, AOGncol, -, AngleOrderingUse;
    F ∈ int_angle A O B     by H2', -, InteriorTransitivity;
  qed     by angles, H2', -, FintAOG, AngleOrdering_DEF;
`;;

let AngleTrichotomy = thm `;
  let α β be point_set;
  assume Angle α ∧ Angle β                              [H1];
  thus (α ≡ β  ∨  α <_ang β  ∨  β <_ang α)  ∧
       ¬(α ≡ β  ∧  α <_ang β)  ∧
       ¬(α ≡ β  ∧  β <_ang α)  ∧
       ¬(α <_ang β  ∧  β <_ang α)

  proof
    ¬(α ≡ β  ∧  α <_ang β)     [Not12] by AngleTrichotomy1;
    ¬(α ≡ β  ∧  β <_ang α)     [Not13] by H1, C5Symmetric, AngleTrichotomy1;
    ¬(α <_ang β  ∧  β <_ang α)     [Not23] by H1, AngleOrderTransitivity, AngleTrichotomy1, C5Reflexive;
    consider P O A such that
    α = ∡ P O A ∧ ¬Collinear P O A     [POA] by H1, ANGLE;
    ¬(P = O) ∧ ¬(O = A)      [Distinct] by -, NonCollinearImpliesDistinct;
    consider a such that
    Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by -, I1;
    P ∉ a     [notPa] by -, Distinct, I1, POA, Collinear_DEF, ∉;
    ∃! r. Ray r ∧ ∃ Q. ¬(O = Q) ∧ r = ray O Q ∧ Q ∉ a ∧ Q,P same_side a ∧ ∡ A O Q ≡ β     by H1, Distinct, a_line, -, C4;
    consider Q such that
    ¬(O = Q) ∧ Q ∉ a ∧ Q,P same_side a ∧ ∡ A O Q ≡ β     [Qexists] by -;
    O ∉ open (Q,P)     [notQOP] by a_line, Qexists, SameSide_DEF, ∉;
    ¬Collinear A O P     [AOPncol] by POA, CollinearSymmetry;
    ¬Collinear A O Q     [AOQncol] by a_line, Distinct, I1, Collinear_DEF, Qexists, ∉;
    Angle (∡ A O P) ∧ Angle (∡ A O Q)     by AOPncol, -, ANGLE;
    α ≡ ∡ A O P  ∧  β ≡ ∡ A O Q  ∧  ∡ A O P ≡ α     [flip] by H1, -, POA, AngleSymmetry, C5Reflexive, Qexists, C5Symmetric;
    cases;
    suppose Collinear Q O P;
      Collinear O P Q by -, CollinearSymmetry;
      Q ∈ ray O P ━ O     by Distinct, -, notQOP, IN_Ray, Qexists, IN_DELETE;
      ray O Q = ray O P     by Distinct, -, RayWellDefined;
      ∡ P O A = ∡ A O Q     by -, Angle_DEF, AngleSymmetry;
      α ≡ β     by -, POA, Qexists;
    qed     by -, Not12, Not13, Not23;
    suppose ¬Collinear Q O P;
      P ∈ int_angle Q O A ∨ Q ∈ int_angle P O A     by Distinct, a_line, Qexists, notPa, -, AngleOrdering;
      P ∈ int_angle A O Q ∨ Q ∈ int_angle A O P     by -, InteriorAngleSymmetry;
      α <_ang ∡ A O Q  ∨  β <_ang ∡ A O P     by H1, AOQncol, AOPncol, -, flip, AngleOrdering_DEF;
      α <_ang β  ∨  β <_ang α     by H1, -, Qexists, flip, AngleTrichotomy2;
    qed     by -, Not12, Not13, Not23;
  end;
`;;

let SupplementExists = thm `;
  let α be point_set;
  assume Angle α                [H1];
  thus ∃ α'. α suppl α'

  proof
    consider A O B such that
    α = ∡ A O B ∧ ¬Collinear A O B ∧ ¬(A = O)    [def_α] by H1, ANGLE, NonCollinearImpliesDistinct;
    consider A' such that
    O ∈ open (A,A')     by -, B2';
    ∡ A O B  suppl  ∡ A' O B     [AOBsup] by def_α, -, SupplementaryAngles_DEF, AngleSymmetry;
  qed     by -, def_α;
`;;

let SupplementImpliesAngle = thm `;
  let α β be point_set;
  assume α suppl β              [H1];
  thus Angle α ∧ Angle β

  proof
    consider A O B A' such that
    ¬Collinear A O B  ∧  O ∈ open (A,A')  ∧  α = ∡ A O B  ∧  β = ∡ B O A'     [H1'] by H1, SupplementaryAngles_DEF;
    ¬(O = A') ∧ Collinear A O A'     [Distinct] by -, NonCollinearImpliesDistinct, B1';
    ¬Collinear B O A'     by H1', CollinearSymmetry, -, NoncollinearityExtendsToLine;
  qed     by H1', -, ANGLE;
`;;

let RightImpliesAngle = thm `;
  ∀ α: point_set. Right α  ⇒  Angle α
  by RightAngle_DEF, SupplementImpliesAngle;
`;;

let SupplementSymmetry = thm `;
  let α β be point_set;
  assume α suppl β [H1];
  thus β suppl α

  proof
  consider A O B A' such that
  ¬Collinear A O B  ∧  O ∈ open (A,A')  ∧  α = ∡ A O B  ∧  β = ∡ B O A'     [H1'] by H1, SupplementaryAngles_DEF;
  ¬(O = A') ∧ Collinear A O A'     by -, NonCollinearImpliesDistinct, B1';
  ¬Collinear A' O B     [A'OBncol] by H1', CollinearSymmetry, -, NoncollinearityExtendsToLine;
  O ∈ open (A',A)  ∧  β = ∡ A' O B  ∧  α = ∡ B O A by H1', B1',  AngleSymmetry;
  qed     by A'OBncol, -, SupplementaryAngles_DEF;
`;;

let SupplementsCongAnglesCong = thm `;
  let α β α' β' be point_set;
  assume α suppl α'  ∧  β suppl β'      [H1];
  assume α ≡ β                  [H2];
  thus α' ≡ β'

  proof
    consider A O B A' such that
    ¬Collinear A O B  ∧  O ∈ open (A,A')  ∧  α = ∡ A O B  ∧  α' = ∡ B O A'     [def_α] by H1, SupplementaryAngles_DEF;
    ¬(A = O) ∧ ¬(O = B) ∧ ¬(A = A') ∧ ¬(O = A') ∧ Collinear A O A'     [Distinctα] by -, NonCollinearImpliesDistinct, B1';
    ¬Collinear B A A' ∧ ¬Collinear O A' B     [BAA'ncol] by def_α, CollinearSymmetry, -, NoncollinearityExtendsToLine;
    Segment (seg O A) ∧ Segment (seg O B) ∧ Segment (seg O A')     [Osegments] by Distinctα, SEGMENT;
    consider C P D C' such that
    ¬Collinear C P D  ∧  P ∈ open (C,C')  ∧  β = ∡ C P D  ∧  β' = ∡ D P C'     [def_β] by H1, SupplementaryAngles_DEF;
    ¬(C = P) ∧ ¬(P = D) ∧ ¬(P = C')     [Distinctβ] by def_β, NonCollinearImpliesDistinct, B1';
    consider X such that
    X ∈ ray P C ━ P  ∧  seg P X ≡ seg O A     [defX] by Osegments, Distinctβ, C1;
    consider Y such that
    Y ∈ ray P D ━ P  ∧  seg P Y ≡ seg O B  ∧  ¬(Y = P)     [defY] by Osegments, Distinctβ, C1, IN_DELETE;
    consider X' such that
    X' ∈ ray P C' ━ P  ∧  seg P X' ≡ seg O A'     [defX'] by Osegments, Distinctβ, C1;
    P ∈ open (X',C)  ∧  P ∈ open (X,X')       [XPX'] by def_β, -, OppositeRaysIntersect1pointHelp, defX;
    ¬(X = P) ∧ ¬(X' = P) ∧ Collinear X P X' ∧ ¬(X = X') ∧ ray A' O = ray A' A ∧ ray X' P = ray X' X     [XPX'line] by defX, defX', IN_DELETE, -, B1', def_α, IntervalRay;
     Collinear P D Y ∧ Collinear P C X     by defY, defX, IN_DELETE, IN_Ray;
    ¬Collinear C P Y ∧ ¬Collinear X P Y     [XPYncol] by def_β, -, defY, NoncollinearityExtendsToLine, CollinearSymmetry, XPX'line;
    ¬Collinear Y X X' ∧ ¬Collinear P X' Y     [YXX'ncol] by -, CollinearSymmetry, XPX', XPX'line, NoncollinearityExtendsToLine;
    ray P X = ray P C  ∧  ray P Y = ray P D  ∧  ray P X' = ray P C'     [equalPrays] by Distinctβ, defX, defY, defX', RayWellDefined;
    β = ∡ X P Y  ∧  β' = ∡ Y P X'  ∧  ∡ A O B ≡ ∡ X P Y     [AOBeqXPY] by def_β, -, Angle_DEF, H2, def_α;
   seg O A ≡ seg P X  ∧  seg O B ≡ seg P Y  ∧  seg A' O ≡ seg X' P     [OAeq] by Osegments, XPX'line, SEGMENT, defX, defY, defX', C2Symmetric, SegmentSymmetry;
    seg A A' ≡ seg X X'     [AA'eq] by def_α, XPX'line, XPX', -, SegmentSymmetry, C3;
    A,O,B ≅ X,P,Y     by def_α, XPYncol, OAeq, AOBeqXPY, SAS;
    seg A B ≡ seg X Y  ∧  ∡ B A O ≡ ∡ Y X P     [AOB≅] by -, TriangleCong_DEF, AngleSymmetry;
    ray A O = ray A A'  ∧  ray X P = ray X  X'  ∧  ∡ B A A' ≡ ∡ Y X X'     by def_α, XPX', IntervalRay, -, Angle_DEF;
    B,A,A' ≅ Y,X,X'     by BAA'ncol, YXX'ncol, AOB≅, -, AA'eq, -, SAS;
    seg A' B ≡ seg X' Y  ∧  ∡ A A' B ≡ ∡ X X' Y     by -, TriangleCong_DEF, SegmentSymmetry;
    O,A',B ≅ P,X',Y     by BAA'ncol, YXX'ncol, OAeq, -, XPX'line, Angle_DEF, SAS;
    ∡ B O A' ≡ ∡ Y P X'     by -, TriangleCong_DEF;
  qed     by -, equalPrays, def_β, Angle_DEF, def_α;
`;;

let SupplementUnique = thm `;
  ∀ α β β': point_set. α suppl β  ∧   α suppl β'  ⇒  β ≡ β'
  by SupplementaryAngles_DEF, ANGLE, C5Reflexive, SupplementsCongAnglesCong;
`;;

let CongRightImpliesRight = thm `;
  let α β be point_set;
  assume Angle α  ∧  Right β            [H1];
  assume α ≡ β                          [H2];
  thus Right α

  proof
    consider α' β' such that
    α suppl α'  ∧  β suppl β'  ∧  β ≡ β'     [suppl] by H1, SupplementExists, H1, RightAngle_DEF;
    α' ≡ β'     [α'eqβ'] by suppl, H2, SupplementsCongAnglesCong;
    Angle β ∧ Angle α' ∧ Angle β'     by suppl, SupplementImpliesAngle;
    α ≡ α' by     H1, -, H2, suppl, α'eqβ', C5Symmetric, C5Transitive;
  qed     by suppl, -, RightAngle_DEF;
`;;

let RightAnglesCongruentHelp = thm `;
  let A O B A' P be point;
  let a be point_set;
  assume ¬Collinear A O B  ∧  O ∈ open (A,A')                   [H1];
  assume Right (∡ A O B)  ∧  Right (∡ A O P)                    [H2];
  thus P ∉ int_angle A O B

  proof
    assume ¬(P ∉ int_angle A O B);
    P ∈ int_angle A O B     [PintAOB] by -, ∉;
    B ∈ int_angle P O A'  ∧  B ∈ int_angle A' O P     [BintA'OP] by H1, -, InteriorReflectionInterior, InteriorAngleSymmetry ;
    ¬Collinear A O P ∧ ¬Collinear P O A'     [AOPncol] by PintAOB, InteriorEZHelp, -, IN_InteriorAngle;
    ∡ A O B suppl ∡ B O A'  ∧  ∡ A O P suppl ∡ P O A'     [AOBsup] by H1, -, SupplementaryAngles_DEF;
    consider α' β' such that
    ∡ A O B suppl α'  ∧  ∡ A O B ≡ α'  ∧  ∡ A O P suppl β'  ∧  ∡ A O P ≡ β'     [supplα'] by H2, RightAngle_DEF;
    α' ≡ ∡ B O A'  ∧  β' ≡ ∡ P O A'     [α'eqA'OB] by -, AOBsup, SupplementUnique;
    Angle (∡ A O B) ∧ Angle α' ∧ Angle (∡ B O A') ∧ Angle (∡ A O P) ∧ Angle β' ∧ Angle (∡ P O A')     [angles] by AOBsup, supplα', SupplementImpliesAngle, AngleSymmetry;
    ∡ A O B ≡ ∡ B O A'  ∧  ∡ A O P ≡ ∡ P O A'     [H2'] by -, supplα', α'eqA'OB, C5Transitive;
    ∡ A O P ≡ ∡ A O P  ∧  ∡ B O A' ≡ ∡ B O A'     [refl] by angles, C5Reflexive;
    ∡ A O P <_ang ∡ A O B  ∧  ∡ B O A' <_ang ∡ P O A'     [BOA'lessPOA'] by angles, H1, PintAOB, -, AngleOrdering_DEF, AOPncol, CollinearSymmetry, BintA'OP, AngleSymmetry;
    ∡ A O P <_ang ∡ B O A'     by -, angles, H2', AngleTrichotomy2;
    ∡ A O P <_ang ∡ P O A'     by -, BOA'lessPOA', AngleOrderTransitivity;
  qed     by -, H2', AngleTrichotomy1;
`;;

let RightAnglesCongruent = thm `;
  let α β be point_set;
  assume Right α ∧ Right β [H1];
   thus α ≡ β

  proof
    consider α' such that
    α suppl α'  ∧  α ≡ α'     by H1, RightAngle_DEF;
    consider A O B A' such that
    ¬Collinear A O B  ∧  O ∈ open (A,A')  ∧  α = ∡ A O B  ∧  α' = ∡ B O A'     [def_α] by -, SupplementaryAngles_DEF;
    ¬(A = O) ∧ ¬(O = B)     [Distinct] by def_α, NonCollinearImpliesDistinct, B1';
    consider a such that
    Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by Distinct, I1;
    B ∉ a     [notBa] by -, def_α, Collinear_DEF, ∉;
    Angle β     by H1, RightImpliesAngle;
    ∃! r. Ray r ∧ ∃ P. ¬(O = P) ∧ r = ray O P ∧ P ∉ a ∧ P,B same_side a ∧ ∡ A O P ≡ β     by -, Distinct, a_line, notBa, C4;
    consider P such that
    ¬(O = P) ∧ P ∉ a ∧ P,B same_side a ∧ ∡ A O P ≡ β     [defP] by -;
    O ∉ open (P,B)     [notPOB] by a_line, -, SameSide_DEF, ∉;
    ¬Collinear A O P     [AOPncol] by a_line, Distinct, I1, defP, Collinear_DEF, ∉;
    Right (∡ A O P)     [AOPright] by -, ANGLE, H1, defP, CongRightImpliesRight;
    P ∉ int_angle A O B  ∧  B ∉ int_angle A O P     by def_α, H1, -, AOPncol, AOPright, RightAnglesCongruentHelp;
    Collinear P O B     by Distinct, a_line, defP, notBa, -, AngleOrdering, InteriorAngleSymmetry, ∉;
    P ∈ ray O B ━ O     by Distinct, -, CollinearSymmetry, notPOB, IN_Ray, defP, IN_DELETE;
    ray O P = ray O B  ∧  ∡ A O P = ∡ A O B     by Distinct, -, RayWellDefined, Angle_DEF;
  qed     by -, defP, def_α;
`;;

let OppositeRightAnglesLinear = thm `;
  let A B O H be point;
  let h be point_set;
  assume ¬Collinear A O H ∧ ¬Collinear H O B                    [H0];
  assume Right (∡ A O H) ∧ Right (∡ H O B)                      [H1];
  assume Line h ∧ O ∈ h ∧ H ∈ h  ∧  ¬(A,B same_side h)          [H2];
  thus O ∈ open (A,B)

  proof
    ¬(A = O) ∧ ¬(O = H) ∧ ¬(O = B)     [Distinct] by  H0, NonCollinearImpliesDistinct;
    A ∉ h ∧ B ∉ h     [notABh] by H0, H2, Collinear_DEF, ∉;
    consider E such that
    O ∈ open (A,E) ∧ ¬(E = O)     [AOE] by Distinct, B2', B1';
    ∡ A O H  suppl  ∡ H O E     [AOHsupplHOE] by H0, -, SupplementaryAngles_DEF;
    E ∉ h     [notEh] by H2, ∉, AOE, BetweenLinear, notABh;
    ¬(A,E same_side  h)     by H2, AOE, SameSide_DEF;
    B,E same_side  h     [Bsim_hE] by H2, notABh, notEh, -, H2, AtMost2Sides;
    consider α' such that
    ∡ A O H  suppl  α'  ∧  ∡ A O H ≡ α'     [AOHsupplα'] by H1, RightAngle_DEF;
    Angle (∡ H O B) ∧ Angle (∡ A O H) ∧ Angle α' ∧ Angle (∡ H O E)     [angα'] by H1, RightImpliesAngle, -, AOHsupplHOE, SupplementImpliesAngle;
    ∡ H O B ≡ ∡ A O H  ∧  α' ≡ ∡ H O E     by H1, RightAnglesCongruent, AOHsupplα', AOHsupplHOE, SupplementUnique;
    ∡ H O B ≡ ∡ H O E     by angα', -, AOHsupplα', C5Transitive;
    ray O B = ray O E     by H2, Distinct, notABh, notEh, Bsim_hE, -, C4Uniqueness;
    B ∈ ray O E ━ O     by Distinct, EndpointInRay, -, IN_DELETE;
  qed     by AOE, -, OppositeRaysIntersect1pointHelp, B1';
`;;

let RightImpliesSupplRight = thm `;
  let A O B A' be point;
  assume ¬Collinear A O B                       [H1];
  assume O ∈ open (A,A')                        [H2];
  assume Right (∡ A O B)                        [H3];
  thus Right (∡ B O A')

  proof
    ∡ A O B suppl ∡ B O A'  ∧  Angle (∡ A O B)  ∧  Angle (∡ B O A')     [AOBsuppl] by H1, H2, SupplementaryAngles_DEF, SupplementImpliesAngle;
    consider β such that
    ∡ A O B suppl β ∧ ∡ A O B ≡ β     [βsuppl] by H3, RightAngle_DEF;
    Angle β  ∧  β ≡ ∡ A O B     [angβ] by -, SupplementImpliesAngle, C5Symmetric;
    ∡ B O A' ≡ β     by AOBsuppl, βsuppl, SupplementUnique;
    ∡ B O A' ≡ ∡ A O B     by AOBsuppl, angβ, -, βsuppl, C5Transitive;
  qed     by AOBsuppl, H3, -, CongRightImpliesRight;
`;;

let IsoscelesCongBaseAngles = thm `;
  let A B C be point;
  assume ¬Collinear A B C       [H1];
  assume seg B A ≡ seg B C      [H2];
  thus  ∡ C A B  ≡ ∡ A C B

  proof
    ¬(A = B) ∧ ¬(B = C) ∧ ¬Collinear C B A     [CBAncol] by H1, NonCollinearImpliesDistinct, CollinearSymmetry;
    seg B C ≡ seg B A  ∧  ∡ A B C ≡ ∡ C B A     by -, SEGMENT, H2, C2Symmetric, H1, ANGLE, AngleSymmetry, C5Reflexive;
    A,B,C ≅ C,B,A     by H1, CBAncol, H2, -, SAS;
  qed     by -, TriangleCong_DEF;
`;;

let C4withC1 = thm `;
  let α l be point_set;
  let O A Y P Q be point;
  assume Angle α ∧ ¬(O = A) ∧ ¬(P = Q)                  [H1];
  assume Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l                [l_line];
  thus ∃ N. ¬(O = N) ∧ N ∉ l ∧ N,Y same_side l ∧ seg O N ≡ seg P Q ∧ ∡ A O N ≡ α

  proof
    ∃! r. Ray r ∧ ∃ B. ¬(O = B) ∧ r = ray O B ∧ B ∉ l ∧ B,Y same_side l ∧ ∡ A O B ≡ α     by H1, l_line, C4;
    consider B such that
    ¬(O = B) ∧ B ∉ l ∧ B,Y same_side l ∧ ∡ A O B ≡ α     [Bexists] by -;
    consider N such that
    N ∈ ray O B ━ O  ∧  seg O N ≡ seg P Q     [Nexists] by H1, -, SEGMENT, C1;
    ¬(O = N)     [notON] by -, IN_DELETE;
    N ∉ l ∧ N,B same_side l     [notNl] by l_line, Bexists, Nexists, RaySameSide;
    N,Y same_side l     [Nsim_lY] by l_line, -, Bexists, SameSideTransitive;
    ray O N = ray O B  ∧  ∡ A O N ≡ α     by Bexists, Nexists, RayWellDefined, Angle_DEF;
  qed     by notON, notNl, Nsim_lY, Nexists, -;
`;;

let C4OppositeSide = thm `;
  let α l be point_set;
  let O A Z P Q be point;
  assume Angle α ∧ ¬(O = A) ∧ ¬(P = Q)                  [H1];
  assume Line l ∧ O ∈ l ∧ A ∈ l ∧ Z ∉ l                 [l_line];
  thus ∃ N. ¬(O = N) ∧ N ∉ l ∧ ¬(Z,N same_side l) ∧ seg O N ≡ seg P Q ∧ ∡ A O N ≡ α

  proof
    ¬(Z = O)     by l_line, ∉;
    consider Y such that
    O ∈ open (Z,Y)     [ZOY] by -, B2';
    ¬(O = Y) ∧ Collinear Z O Y     by -, B1';
    Y ∉ l     [notYl] by l_line, I1, -, Collinear_DEF, ∉;
    consider N such that
    ¬(O = N) ∧ N ∉ l  ∧  N,Y same_side l  ∧ seg O N ≡ seg P Q  ∧  ∡ A O N ≡ α     [Nexists] by H1, l_line, notYl, C4withC1;
    ¬(Z,Y same_side l)     by l_line, ZOY, SameSide_DEF;
    ¬(Z,N same_side l)     by l_line, Nexists, notYl, -, SameSideTransitive;
  qed by -, Nexists;
`;;

let SSS = thm `;
  let A B C A' B' C' be point;
  assume ¬Collinear A B C ∧ ¬Collinear A' B' C'                                 [H1];
  assume seg A B ≡ seg A' B'  ∧  seg A C ≡ seg A' C'  ∧  seg B C ≡ seg B' C'            [H2];
  thus A,B,C ≅ A',B',C'

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬(A' = B') ∧ ¬(B' = C')     [Distinct] by H1, NonCollinearImpliesDistinct;
    consider h such that
    Line h ∧ A ∈ h ∧ C ∈ h     [h_line] by Distinct, I1;
    B ∉ h     [notBh] by h_line, H1, ∉, Collinear_DEF;
    Segment (seg A B) ∧ Segment (seg C B) ∧ Segment (seg A' B') ∧ Segment (seg C' B')     [segments] by Distinct, -, SEGMENT;
    Angle (∡ C' A' B')     by H1, CollinearSymmetry, ANGLE;
    consider N such that
    ¬(A = N) ∧ N ∉ h ∧ ¬(B,N same_side h) ∧ seg A N ≡ seg A' B'  ∧  ∡ C A N ≡ ∡ C' A' B'     [Nexists] by -, Distinct, h_line, notBh, C4OppositeSide;
    ¬(C = N)     by h_line, Nexists, ∉;
    Segment (seg A N) ∧ Segment (seg C N)     [segN] by Nexists, -, SEGMENT;
    ¬Collinear A N C     [ANCncol] by h_line, Distinct, I1, Collinear_DEF, Nexists, ∉;
    Angle (∡ A B C) ∧ Angle (∡ A' B' C') ∧ Angle (∡ A N C)     [angles] by H1, -, ANGLE;
    seg A B ≡ seg A N     [ABeqAN] by segments, segN, Nexists, H2, C2Symmetric, C2Transitive;
    C,A,N ≅ C',A',B'     by ANCncol, H1, CollinearSymmetry, H2, Nexists, SAS;
    ∡ A N C ≡ ∡ A' B' C'  ∧  seg C N ≡ seg C' B'     [ANCeq] by -, TriangleCong_DEF;
    seg C B ≡ seg C N     [CBeqCN] by segments, segN, -, H2, SegmentSymmetry, C2Symmetric, C2Transitive;
    consider G such that
    G ∈ h ∧ G ∈ open (B,N)     [BGN] by Nexists, h_line, SameSide_DEF;
    ¬(B = N)     [notBN] by -, B1';
    ray B G = ray B N  ∧  ray N G = ray N B     [Grays] by BGN, B1', IntervalRay;
    consider v such that
    Line v ∧ B ∈ v ∧ N ∈ v     [v_line] by notBN, I1;
    G ∈ v ∧ ¬(h = v)     by v_line, BGN, BetweenLinear, notBh, ∉;
    h ∩ v = {G}     [hvG] by h_line, v_line, -, BGN, I1Uniqueness;
    ¬(G = A)  ⇒  ∡ A B G ≡ ∡ A N G [ABGeqANG]
    proof
      assume ¬(G = A) [notGA];
      A ∉ v     by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE;
      ¬Collinear B A N     by v_line, notBN, I1, Collinear_DEF, -, ∉;
      ∡ N B A ≡ ∡ B N A     by -, ABeqAN, IsoscelesCongBaseAngles;
      ∡ G B A ≡ ∡ G N A     by -, Grays, Angle_DEF, notGA;
    qed by -, AngleSymmetry;
    ¬(G = C)  ⇒  ∡ G B C ≡ ∡ G N C [GBCeqGNC]
    proof
      assume ¬(G = C) [notGC];
      C ∉ v     by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE;
      ¬Collinear B C N     by v_line, notBN, I1, Collinear_DEF, -, ∉;
      ∡ N B C ≡ ∡ B N C     by -, CBeqCN, IsoscelesCongBaseAngles, AngleSymmetry;
    qed     by -, Grays, Angle_DEF;
    ∡ A B C ≡ ∡ A N C
    proof
      cases;
      suppose G = A     [GA];
        ¬(G = C)     by -, Distinct;
      qed     by -, GBCeqGNC, GA;
      suppose G = C     [GC];
        ¬(G = A)     by -, Distinct;
      qed     by -, ABGeqANG, GC;
      suppose ¬(G = A) ∧ ¬(G = C)     [AGCdistinct];
        ∡ A B G ≡ ∡ A N G  ∧  ∡ G B C ≡ ∡ G N C     [Gequivs] by -, ABGeqANG, GBCeqGNC;
        ¬Collinear G B C ∧ ¬Collinear G N C ∧ ¬Collinear G B A ∧ ¬Collinear G N A     [Gncols] by h_line, BGN, AGCdistinct, I1, Collinear_DEF, notBh, Nexists, ∉;
        Collinear A G C     by h_line, BGN, Collinear_DEF;
        G ∈ open (A,C) ∨ C ∈ open (G,A) ∨ A ∈ open (C,G)     by Distinct, AGCdistinct, -, B3';
        cases by -;
        suppose G ∈ open (A,C);
          G ∈ int_angle A B C  ∧  G ∈ int_angle A N C     by H1, ANCncol, -, ConverseCrossbar;
        qed     by -, Gequivs, AngleAddition;
        suppose C ∈ open (G,A);
          C ∈ int_angle G B A  ∧  C ∈ int_angle G N A     by Gncols, -, B1', ConverseCrossbar;
        qed     by -, Gequivs, AngleSubtraction, AngleSymmetry;
        suppose A ∈ open (C,G);
          A ∈ int_angle G B C  ∧  A ∈ int_angle G N C     by Gncols, -, B1', ConverseCrossbar;
        qed     by -, Gequivs, AngleSymmetry, AngleSubtraction;
      end;
    end;
    ∡ A B C ≡ ∡ A' B' C'     by angles, -, ANCeq, C5Transitive;
  qed     by H1, H2, SegmentSymmetry, -, SAS;
`;;

let AngleBisector = thm `;
  let A B C be point;
  assume ¬Collinear B A C                                       [H1];
  thus ∃ F. F ∈ int_angle B A C  ∧  ∡ B A F ≡ ∡ F A C

  proof
    ¬(A = B) ∧ ¬(A = C)     [Distinct] by H1, NonCollinearImpliesDistinct;
    consider D such that
    B ∈ open (A,D)     [ABD] by Distinct, B2';
    ¬(A = D) ∧ Collinear A B D ∧ Segment (seg A D)     [ABD'] by -, B1', SEGMENT;
    consider E such that
    E ∈ ray A C ━ A  ∧  seg A E ≡ seg A D  ∧  ¬(A = E)     [ErAC] by -, Distinct, C1, IN_DELETE, IN_Ray;
    Collinear A C E  ∧  D ∈ ray A B ━ A     [notAE] by ErAC, IN_DELETE, IN_Ray, ABD, IntervalRayEZ;
    ray A D = ray A B  ∧  ray A E =  ray A C     [equalrays] by Distinct, notAE, ErAC, RayWellDefined;
    ¬Collinear D A E ∧ ¬Collinear E A D ∧ ¬Collinear A E D     [EADncol] by H1, ABD', notAE, ErAC, CollinearSymmetry, NoncollinearityExtendsToLine;
    ∡ D E A ≡ ∡ E D A     [DEAeq] by EADncol, ErAC, IsoscelesCongBaseAngles;
    ¬Collinear E D A ∧ Angle (∡ E D A) ∧ ¬Collinear A D E ∧ ¬Collinear D E A     [angEDA] by EADncol, CollinearSymmetry, ANGLE;
    ¬(D = E)     [notDE] by EADncol, NonCollinearImpliesDistinct;
    consider h such that
    Line h ∧ D ∈ h ∧ E ∈ h     [h_line] by -, I1;
    A ∉ h     [notAh] by -, Collinear_DEF, EADncol, ∉;
    consider F such that
    ¬(D = F)  ∧  F ∉ h  ∧  ¬(A,F same_side h)  ∧  seg D F ≡ seg D A  ∧  ∡ E D F ≡ ∡ E D A     [Fexists] by angEDA, notDE, ABD', h_line, -, C4OppositeSide;
    ¬(A = F)     [notAF] by h_line, -, SameSideReflexive;
    ¬Collinear E D F ∧ ¬Collinear D E F ∧ ¬Collinear F E D     [EDFncol] by h_line, notDE, I1, Collinear_DEF, Fexists, ∉;
    seg D E ≡ seg D E  ∧  seg F A ≡ seg F A     [FArefl] by notDE, notAF, SEGMENT, C2Reflexive;
    E,D,F ≅ E,D,A     by EDFncol, angEDA, -, Fexists, SAS;
    seg F E ≡ seg A E ∧ ∡ F E D ≡ ∡ A E D     [FED≅] by -, TriangleCong_DEF, SegmentSymmetry;
    ∡ E D A ≡ ∡ D E A  ∧  ∡ E D A ≡ ∡ E D F  ∧  ∡ D E A ≡ ∡ D E F    [EDAeqEDF] by EDFncol, ANGLE, angEDA, Fexists, FED≅, DEAeq, C5Symmetric, AngleSymmetry;
    consider G such that
    G ∈ h ∧ G ∈ open (A,F)     [AGF] by Fexists, h_line, SameSide_DEF;
    F ∈ ray A G ━ A     [FrAG] by -, IntervalRayEZ;
    consider v such that
    Line v ∧ A ∈ v ∧ F ∈ v ∧ G ∈ v     [v_line] by notAF, I1, AGF, BetweenLinear;
    ¬(v = h)  ∧  v ∩ h = {G}     [vhG] by -, notAh, ∉, h_line, AGF, I1Uniqueness;
    D ∉ v     [notDv]
    proof
      assume ¬(D ∉ v);
      D ∈ v  ∧  D = G     [DG] by h_line, -, ∉, vhG, IN_INTER, IN_SING;
      D ∈ open (A,F)     by DG, AGF;
      ∡ E D A suppl ∡ E D F     [EDAsuppl] by angEDA, -, SupplementaryAngles_DEF, AngleSymmetry;
      Right (∡ E D A)     by EDAsuppl, EDAeqEDF, RightAngle_DEF;
      Right (∡ A E D)     [RightAED] by angEDA, ANGLE, -, DEAeq, CongRightImpliesRight, AngleSymmetry;
      Right (∡ D E F)     by EDFncol, ANGLE, -, FED≅, CongRightImpliesRight, AngleSymmetry;
      E ∈ open (A,F)     by EADncol, EDFncol, RightAED, -, h_line, Fexists,  OppositeRightAnglesLinear;
      E ∈ v  ∧  E = G     by v_line, -, BetweenLinear, h_line, vhG, IN_INTER, IN_SING;
    qed     by -, DG, notDE;
    E ∉ v     [notEv]
    proof
      assume ¬(E ∉ v);
      E ∈ v  ∧  E = G     [EG] by h_line, -, ∉, vhG, IN_INTER, IN_SING;
      E ∈ open (A,F)     by -, AGF;
      ∡ D E A suppl ∡ D E F     [DEAsuppl] by EADncol, -, SupplementaryAngles_DEF, AngleSymmetry;
      Right (∡ D E A)     [RightDEA] by DEAsuppl, EDAeqEDF, RightAngle_DEF;
      Right (∡ E D A)     [RightEDA] by angEDA, RightDEA, EDAeqEDF, CongRightImpliesRight;
      Right (∡ E D F)     by EDFncol, ANGLE, RightEDA, Fexists, CongRightImpliesRight;
      D ∈ open (A,F)     by angEDA, EDFncol, RightEDA, AngleSymmetry, -, h_line, Fexists,  OppositeRightAnglesLinear;
      D ∈ v ∧ D = G     by v_line, -, BetweenLinear, h_line, vhG, IN_INTER, IN_SING;
    qed     by -, EG, notDE;
    ¬Collinear F A E ∧ ¬Collinear F A D  ∧  ¬(F = E)     [FAEncol] by v_line, notAF, I1, Collinear_DEF, notEv, notDv, ∉, NonCollinearImpliesDistinct;
    seg F E ≡ seg A D     [FEeqAD] by -, ErAC, ABD', SEGMENT, FED≅, ErAC, C2Transitive;
    seg A D ≡ seg F D     by SegmentSymmetry, ABD', Fexists, SEGMENT, C2Symmetric;
    seg F E ≡ seg F D     by FAEncol, ABD', Fexists, SEGMENT, FEeqAD, -, C2Transitive;
    F,A,E ≅ F,A,D     by FAEncol, FArefl, -, ErAC, SSS;
    ∡ F A E ≡ ∡ F A D     [FAEeq] by -, TriangleCong_DEF;
    ∡ D A F ≡ ∡ F A E     by FAEncol, ANGLE, FAEeq, C5Symmetric, AngleSymmetry;
    ∡ B A F ≡ ∡ F A C     [BAFeqFAC] by -, equalrays, Angle_DEF;
    ¬(E,D same_side v)
    proof
      assume E,D same_side v;
      ray A D = ray A E     by v_line, notAF, notDv, notEv, -, FAEeq, C4Uniqueness;
    qed by ABD', EndpointInRay, -, IN_Ray, EADncol;
    consider H such that
    H ∈ v ∧ H ∈ open (E,D)     [EHD] by v_line, -, SameSide_DEF;
    H = G     by -, h_line, BetweenLinear, IN_INTER, vhG, IN_SING;
    G ∈ int_angle E A D     [GintEAD] by EADncol,  -, EHD, ConverseCrossbar;
    F ∈ int_angle E A D     [FintEAD] by GintEAD, FrAG, WholeRayInterior;
    B ∈ ray A D ━ A   ∧   C ∈ ray A E ━ A     by equalrays, Distinct, EndpointInRay, IN_DELETE;
    F ∈ int_angle B A C     by FintEAD, -, InteriorWellDefined, InteriorAngleSymmetry;
  qed     by -, BAFeqFAC;
`;;

let EuclidPropositionI_6 = thm `;
  let A B C be point;
  assume ¬Collinear A B C                       [H1];
  assume ∡ B A C ≡ ∡ B C A                      [H2];
  thus seg B A ≡ seg B C

  proof
    ¬(A = C)     by H1, NonCollinearImpliesDistinct;
    seg C A ≡ seg A C     [CAeqAC] by SegmentSymmetry, -, SEGMENT, C2Reflexive;
    ¬Collinear B C A ∧ ¬Collinear C B A ∧ ¬Collinear B A C     [BCAncol] by H1, CollinearSymmetry;
    ∡ A C B ≡ ∡ C A B     by -, ANGLE, H2, C5Symmetric, AngleSymmetry;
    C,B,A ≅ A,B,C     by H1, BCAncol, CAeqAC, H2, -, ASA;
  qed by -, TriangleCong_DEF;
`;;

let IsoscelesExists = thm `;
  let A B be point;
  assume ¬(A = B)                                       [H1];
  thus ∃ D. ¬Collinear A D B  ∧  seg D A ≡ seg D B

  proof
    consider l such that
    Line l ∧ A ∈ l ∧ B ∈ l     [l_line] by H1, I1;
    consider C such that
    C ∉ l     [notCl] by -, ExistsPointOffLine;
    ¬Collinear C A B ∧ ¬Collinear C B A ∧ ¬Collinear A B C ∧ ¬Collinear A C B ∧ ¬Collinear B A C     [CABncol] by l_line, H1, I1, Collinear_DEF, -, ∉;
    ∡ C A B ≡ ∡ C B A  ∨  ∡ C A B <_ang ∡ C B A  ∨  ∡ C B A <_ang ∡ C A B     by -, ANGLE, AngleTrichotomy;
    cases by -;
    suppose ∡ C A B ≡ ∡ C B A;
    qed     by -, CABncol, EuclidPropositionI_6;
    suppose ∡ C A B <_ang ∡ C B A;
      ∡ C A B <_ang ∡ A B C     by -, AngleSymmetry;
      consider E such that
      E ∈ int_angle A B C  ∧  ∡ C A B ≡ ∡ A B E     [Eexists] by CABncol, ANGLE, -, AngleOrderingUse;
      ¬(B = E)     [notBE] by -, InteriorEZHelp;
      consider D such that
      D ∈ open (A,C)  ∧  D ∈ ray B E ━ B     [Dexists] by Eexists, Crossbar_THM;
      D ∈ int_angle A B C     by Eexists, -, WholeRayInterior;
      ¬Collinear A D B     [ADBncol] by -, InteriorEZHelp, CollinearSymmetry;
      ray B D = ray B E  ∧  ray A D = ray A C     by notBE, Dexists, RayWellDefined, IntervalRay;
      ∡ D A B ≡ ∡ A B D     by Eexists, -, Angle_DEF;
    qed     by ADBncol, -, AngleSymmetry, EuclidPropositionI_6;
    :: similar case
    suppose ∡ C B A <_ang ∡ C A B;
      ∡ C B A <_ang ∡ B A C     by -, AngleSymmetry;
      consider E such that
      E ∈ int_angle B A C  ∧  ∡ C B A ≡ ∡ B A E     [Eexists] by CABncol, ANGLE, -, AngleOrderingUse;
      ¬(A = E)     [notAE] by -, InteriorEZHelp;
      consider D such that
      D ∈ open (B,C) ∧ D ∈ ray A E ━ A     [Dexists] by Eexists, Crossbar_THM;
      D ∈ int_angle B A C     by Eexists, -, WholeRayInterior;
      ¬Collinear A D B ∧ ¬Collinear D A B ∧ ¬Collinear D B A     [ADBncol] by -, InteriorEZHelp, CollinearSymmetry;
      ray A D = ray A E  ∧  ray B D = ray B C     by notAE, Dexists, RayWellDefined, IntervalRay;
      ∡ D B A ≡ ∡ B A D     by Eexists, -, Angle_DEF;
      ∡ D A B ≡ ∡ D B A     by AngleSymmetry,  ADBncol, ANGLE, -, C5Symmetric;
    qed     by ADBncol, -, EuclidPropositionI_6;
  end;
`;;

let MidpointExists = thm `;
  let A B be point;
  assume ¬(A = B)                                       [H1];
  thus ∃ M. M ∈ open (A,B)  ∧  seg A M ≡ seg M B

  proof
    consider D such that
    ¬Collinear A D B  ∧  seg D A ≡ seg D B     [Dexists] by H1, IsoscelesExists;
    consider F such that
    F ∈ int_angle A D B  ∧  ∡ A D F ≡ ∡ F D B     [Fexists] by -, AngleBisector;
    ¬(D = F)     [notDF] by -, InteriorEZHelp;
    consider M such that
    M ∈ open (A,B) ∧  M ∈ ray D F ━ D     [Mexists] by Fexists, Crossbar_THM;
    ray D M = ray D F     by notDF, -, RayWellDefined;
    ∡ A D M ≡ ∡ M D B     [ADMeqMDB] by Fexists, -, Angle_DEF;
    M ∈ int_angle A D B     by Fexists, Mexists, WholeRayInterior;
    ¬(D = M) ∧ ¬Collinear A D M ∧ ¬Collinear B D M     [ADMncol] by -, InteriorEZHelp, InteriorAngleSymmetry;
    seg D M ≡ seg D M     by -, SEGMENT, C2Reflexive;
    A,D,M ≅ B,D,M     by ADMncol, Dexists, -, ADMeqMDB, AngleSymmetry, SAS;
  qed     by Mexists, -, TriangleCong_DEF, SegmentSymmetry;
`;;

let EuclidPropositionI_7short = thm `;
  let A B C D be point;
  let a be point_set;
  assume ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a                      [a_line];
  assume ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧ C,D same_side a             [Csim_aD];
  assume seg A C ≡ seg A D                                      [ACeqAD];
  thus ¬(seg B C ≡ seg B D)

  proof
    ¬(A = C) ∧ ¬(A = D)     [AnotCD] by a_line, Csim_aD, ∉;
    assume seg B C ≡ seg B D;
    seg C B ≡ seg D B  ∧  seg A B ≡ seg A B  ∧  seg A D ≡ seg A D     [segeqs] by -, SegmentSymmetry, a_line, AnotCD, SEGMENT, C2Reflexive;
    ¬Collinear A C B  ∧ ¬Collinear A D B     by a_line, I1, Csim_aD, Collinear_DEF, ∉;
    A,C,B ≅ A,D,B     by -, ACeqAD, segeqs, SSS;
    ∡ B A C ≡ ∡ B A D     by -, TriangleCong_DEF;
    ray A D = ray A C     by a_line, Csim_aD, -, C4Uniqueness;
    C ∈ ray A D ━ A  ∧  D ∈ ray A D ━ A     by AnotCD, -, EndpointInRay, IN_DELETE;
    C = D     by AnotCD, SEGMENT, -, ACeqAD, segeqs, C1;
  qed     by -, Csim_aD;
`;;

let EuclidPropositionI_7Help = thm `;
  let A B C D be point;
  let a be point_set;
  assume ¬(A = B)                                                       [notAB];
  assume Line a ∧ A ∈ a ∧ B ∈ a                                         [a_line];
  assume ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧ C,D same_side a                     [Csim_aD];
  assume seg A C ≡ seg A D                                              [ACeqAD];
  assume C ∈ int_triangle D A B  ∨  ConvexQuadrilateral A B C D         [Int_ConvQuad];
  thus ¬(seg B C ≡ seg B D)

  proof
    ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D)     [Distinct] by a_line, Csim_aD, ∉, SameSide_DEF;
    cases by Int_ConvQuad;
    suppose ConvexQuadrilateral A B C D;
      A ∈ int_angle B C D  ∧  B ∈ int_angle C D A  ∧  Tetralateral A B C D    [ABint] by -, ConvexQuad_DEF, Quadrilateral_DEF;
      ¬Collinear B C D ∧ ¬Collinear D C B ∧ ¬Collinear C B D ∧ ¬Collinear C D A ∧ ¬Collinear D A C ∧ Angle (∡ D C A) ∧ Angle (∡ C D B)     [angCDB] by -, Tetralateral_DEF, CollinearSymmetry, ANGLE;
      ∡ C D A ≡ ∡ D C A     [CDAeqDCA] by angCDB, Distinct, SEGMENT, ACeqAD, C2Symmetric, IsoscelesCongBaseAngles;
      A ∈ int_angle D C B  ∧  ∡ D C A ≡ ∡ D C A  ∧  ∡ C D B ≡ ∡ C D B     by ABint, InteriorAngleSymmetry, angCDB, ANGLE, C5Reflexive;
      ∡ D C A <_ang ∡ D C B  ∧  ∡ C D B <_ang ∡ C D A     by angCDB, ABint, -, AngleOrdering_DEF;
      ∡ C D B <_ang ∡ D C B     by -, angCDB, CDAeqDCA, AngleTrichotomy2, AngleOrderTransitivity;
      ¬(∡ D C B ≡ ∡ C D B)     by -, AngleTrichotomy1, angCDB, ANGLE, C5Symmetric;
    qed     by angCDB, -, IsoscelesCongBaseAngles;
      suppose C ∈ int_triangle D A B;
      C ∈ int_angle A D B  ∧  C ∈ int_angle D A B     [CintADB] by -, IN_InteriorTriangle, InteriorAngleSymmetry;
      ¬Collinear A D C ∧ ¬Collinear B D C     [ADCncol] by CintADB, InteriorEZHelp, InteriorAngleSymmetry;
      ¬Collinear D A C ∧ ¬Collinear C D A ∧ ¬Collinear A C D ∧ ¬Collinear A D C     [DACncol] by -, CollinearSymmetry;
      ¬Collinear B C D ∧ Angle (∡ D C A) ∧ Angle (∡ C D B) ∧ ¬Collinear D C B     [angCDB] by ADCncol, -, CollinearSymmetry, ANGLE;
      ∡ C D A ≡ ∡ D C A     [CDAeqDCA] by DACncol, Distinct, ADCncol, SEGMENT, ACeqAD, C2Symmetric, IsoscelesCongBaseAngles;
      consider E such that
      D ∈ open (A,E) ∧ ¬(D = E) ∧ Collinear A D E     [ADE] by Distinct, B2', B1';
      B ∈ int_angle C D E ∧ Collinear D A E     [BintCDE] by CintADB, -, InteriorReflectionInterior, CollinearSymmetry;
      ¬Collinear C D E     [CDEncol] by DACncol, -, ADE, NoncollinearityExtendsToLine;
      consider F such that
      F ∈ open (B,D)  ∧  F ∈ ray A C ━ A     [Fexists] by CintADB, Crossbar_THM, B1';
      F ∈ int_angle B C D     [FintBCD] by ADCncol, CollinearSymmetry, -, ConverseCrossbar;
      ¬Collinear D C F     [DCFncol] by Distinct, ADCncol, CollinearSymmetry, Fexists, B1', NoncollinearityExtendsToLine;
      Collinear A C F  ∧  F ∈ ray D B ━ D  ∧  C ∈ int_angle A D F     by Fexists, IN_DELETE, IN_Ray, B1', IntervalRayEZ, CintADB, InteriorWellDefined;
      C ∈ open (A,F)     by -, AlternateConverseCrossbar;
      ∡ A D C suppl ∡ C D E  ∧  ∡ A C D suppl ∡ D C F     by ADE, DACncol, -, SupplementaryAngles_DEF;
      ∡ C D E ≡ ∡ D C F     [CDEeqDCF] by -, CDAeqDCA, AngleSymmetry, SupplementsCongAnglesCong;
      ∡ C D B <_ang ∡ C D E     by angCDB, CDEncol, BintCDE, C5Reflexive, AngleOrdering_DEF;
      ∡ C D B <_ang ∡ D C F     [CDBlessDCF] by -, DCFncol, ANGLE, CDEeqDCF, AngleTrichotomy2;
      ∡ D C F <_ang ∡ D C B     by DCFncol, ANGLE, angCDB, FintBCD, InteriorAngleSymmetry, C5Reflexive, AngleOrdering_DEF;
      ∡ C D B <_ang ∡ D C B     by CDBlessDCF, -, AngleOrderTransitivity;
      ¬(∡ D C B ≡ ∡ C D B)     by -, AngleTrichotomy1, angCDB, CollinearSymmetry, ANGLE, C5Symmetric;
    qed     by Distinct, ADCncol, CollinearSymmetry, -, IsoscelesCongBaseAngles;
  end;
`;;

let EuclidPropositionI_7 = thm `;
  let A B C D be point;
  let a be point_set;
  assume ¬(A = B)                                               [notAB];
  assume Line a ∧ A ∈ a ∧ B ∈ a                                 [a_line];
  assume ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧ C,D same_side a             [Csim_aD];
  assume seg A C ≡ seg A D                                      [ACeqAD];
  thus ¬(seg B C ≡ seg B D)

  proof
    ¬Collinear A B C ∧ ¬Collinear D A B     [ABCncol] by a_line, notAB, I1, Collinear_DEF, Csim_aD, ∉;
    ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ A ∉ open (C,D)     [Distinct] by a_line, Csim_aD, ∉, SameSide_DEF;
    ¬Collinear A D C      [ADCncol]
    proof
      assume Collinear A D C;
      C ∈ ray A D ━ A  ∧  D ∈ ray A D ━ A     by Distinct, -, IN_Ray, EndpointInRay, IN_DELETE;
    qed     by Distinct, SEGMENT, -, ACeqAD, C2Reflexive, C1, Csim_aD;
    D,C same_side a     [Dsim_aC] by a_line, Csim_aD, SameSideSymmetric;
    seg A D ≡ seg A C  ∧  seg B D ≡ seg B D     [ADeqAC] by Distinct, SEGMENT, ACeqAD, C2Symmetric, C2Reflexive;
    ¬Collinear D A C ∧ ¬Collinear C D A ∧ ¬Collinear A C D ∧ ¬Collinear A D C     [DACncol] by ADCncol, CollinearSymmetry;
    ¬(seg B D ≡ seg B C)  ⇒  ¬(seg B C ≡ seg B D)     [BswitchDC] by Distinct, SEGMENT, C2Symmetric;
    cases;
    suppose Collinear B D C;
      B ∉ open (C,D)  ∧  C ∈ ray B D ━ B  ∧  D ∈ ray B D ━ B     by a_line, Csim_aD, SameSide_DEF, ∉, Distinct, -, IN_Ray, Distinct, IN_DELETE, EndpointInRay;
    qed     by Distinct, SEGMENT, -, ACeqAD, ADeqAC, C1, Csim_aD;
    suppose ¬Collinear B D C     [BDCncol];
      Tetralateral A B C D     by notAB, Distinct, Csim_aD, ABCncol, -, CollinearSymmetry, DACncol, Tetralateral_DEF;
      ConvexQuadrilateral A B C D  ∨  C ∈ int_triangle D A B  ∨
      ConvexQuadrilateral A B D C  ∨  D ∈ int_triangle C A B     by -, a_line, Csim_aD,  FourChoicesTetralateral, InteriorTriangleSymmetry;
    qed     by notAB, a_line, Csim_aD, Dsim_aC, ACeqAD, ADeqAC, -, EuclidPropositionI_7Help, BswitchDC;
  end;
`;;

let EuclidPropositionI_11 = thm `;
  let A B be point;
  assume ¬(A = B)                       [notAB];
  thus ∃ F. Right (∡ A B F)

  proof
    consider C such that
    B ∈ open (A,C)  ∧  seg B C ≡ seg B A     [ABC] by notAB, SEGMENT, C1OppositeRay;
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C     [Distinct] by ABC, B1';
    seg B A ≡ seg B C     [BAeqBC] by -, SEGMENT, ABC, C2Symmetric;
    consider F such that
    ¬Collinear A F C  ∧  seg F A  ≡ seg F C     [Fexists] by Distinct, IsoscelesExists;
    ¬Collinear B F A ∧ ¬Collinear B F C     [BFAncol] by -, CollinearSymmetry, Distinct, NoncollinearityExtendsToLine;
    ¬Collinear A B F ∧ Angle (∡ A B F)     [angABF] by BFAncol, CollinearSymmetry, ANGLE;
    ∡ A B F suppl ∡ F B C     [ABFsuppl] by -, ABC, SupplementaryAngles_DEF;
    ¬(B = F)  ∧  seg B F ≡ seg B F     by BFAncol, NonCollinearImpliesDistinct, SEGMENT, C2Reflexive;
    B,F,A ≅ B,F,C     by BFAncol, -, BAeqBC, Fexists, SSS;
    ∡ A B F ≡ ∡ F B C     by -, TriangleCong_DEF, AngleSymmetry;
  qed     by angABF, ABFsuppl, -, RightAngle_DEF;
`;;

let DropPerpendicularToLine = thm `;
  let P be point;
  let l be point_set;
  assume Line l  ∧  P ∉ l                       [l_line];
  thus ∃ E Q. E ∈ l ∧ Q ∈ l ∧ Right (∡ P Q E)

  proof
    consider A B such that
    A ∈ l ∧ B ∈ l ∧ ¬(A = B)     [ABl] by l_line, I2;
    ¬Collinear B A P ∧ ¬Collinear P A B ∧ ¬(A = P)     [BAPncol] by l_line, ABl, I1, Collinear_DEF, ∉, CollinearSymmetry, ABl, ∉;
    Angle (∡ B A P) ∧ Angle (∡ P A B)     [angBAP] by -, ANGLE, AngleSymmetry;
    consider P' such that
    ¬(A = P') ∧ P' ∉ l ∧ ¬(P,P' same_side l) ∧ seg A P' ≡ seg A P  ∧  ∡ B A P' ≡ ∡ B A P     [P'exists] by angBAP, ABl, BAPncol, l_line, C4OppositeSide;
    consider Q such that
    Q ∈ l ∧ Q ∈ open (P,P') ∧ Collinear A B Q     [Qexists] by l_line, -, SameSide_DEF, ABl, Collinear_DEF;
    ¬Collinear B A P'     [BAP'ncol] by l_line, ABl, I1, Collinear_DEF, P'exists, ∉;
    ∡ B A P ≡ ∡ B A P'     [BAPeqBAP'] by -, ANGLE, angBAP, P'exists, C5Symmetric;
    ∃ E. E ∈ l  ∧  ¬Collinear P Q E  ∧  ∡ P Q E ≡ ∡ E Q P'
    proof
      cases;
      suppose A = Q [AQ];
     qed     by ABl, AQ, BAPncol, BAPeqBAP', AngleSymmetry;
      suppose ¬(A = Q)     [notAQ];
        seg A Q  ≡ seg A Q  ∧  seg A P ≡ seg A P'     [APeqAP'] by -, SEGMENT, C2Reflexive, BAPncol, P'exists, C2Symmetric;
        ¬Collinear Q A P' ∧ ¬Collinear Q A P     [QAP'ncol] by l_line, ABl, Qexists, notAQ, I1, Collinear_DEF, P'exists, ∉;
        ∡ Q A P ≡ ∡ Q A P'
        proof
          cases;
          suppose A ∈ open (Q,B);
            ∡ B A P suppl ∡ P A Q   ∧  ∡ B A P' suppl ∡ P' A Q     by BAPncol, BAP'ncol, -, B1',  SupplementaryAngles_DEF;
          qed     by -, BAPeqBAP', SupplementsCongAnglesCong, AngleSymmetry;
          suppose ¬(A ∈ open (Q,B));
            A ∉ open (Q,B)  ∧  Q ∈ ray A B ━ A  ∧  ray A Q = ray A B     by -, ∉, ABl, Qexists, IN_Ray, notAQ, IN_DELETE, ABl, RayWellDefined;
          qed     by -, BAPeqBAP', Angle_DEF;
        end;
        Q,A,P ≅ Q,A,P'     by QAP'ncol, APeqAP', -, SAS;
      qed     by -, TriangleCong_DEF, AngleSymmetry, ABl, QAP'ncol, CollinearSymmetry;
    end;
    consider E such that
    E ∈ l ∧ ¬Collinear P Q E ∧ ∡ P Q E ≡ ∡ E Q P'     [Eexists] by -;
    ∡ P Q E suppl ∡ E Q P'  ∧  Right (∡ P Q E)     by -, Qexists, SupplementaryAngles_DEF, RightAngle_DEF;
  qed     by Eexists, Qexists, -;
`;;

let EuclidPropositionI_14 = thm `;
  let A B C D be point;
  let l be point_set;
  assume Line l ∧ A ∈ l ∧ B ∈ l ∧ ¬(A = B)              [l_line];
  assume C ∉ l ∧ D ∉ l ∧ ¬(C,D same_side l)             [Cnsim_lD];
  assume ∡ C B A suppl ∡ A B D                  [CBAsupplABD];
  thus B ∈ open (C,D)

  proof
    ¬(B = C) ∧ ¬(B = D) ∧ ¬Collinear C B A     [Distinct] by l_line, Cnsim_lD, ∉, I1, Collinear_DEF;
    consider E such that
    B ∈ open (C,E)     [CBE] by Distinct, B2';
    E ∉ l ∧ ¬(C,E same_side l)     [Csim_lE] by l_line, ∉, -, BetweenLinear, Cnsim_lD, SameSide_DEF;
    D,E same_side l     [Dsim_lE] by l_line, Cnsim_lD, -, AtMost2Sides;
    ∡ C B A suppl ∡ A B E     by Distinct, CBE, SupplementaryAngles_DEF;
    ∡ A B D ≡ ∡ A B E     by CBAsupplABD, -, SupplementUnique;
    ray B E = ray B D     by l_line, Csim_lE, Cnsim_lD, Dsim_lE, -, C4Uniqueness;
    D ∈ ray B E ━ B     by Distinct, -, EndpointInRay, IN_DELETE;
  qed     by CBE, -, OppositeRaysIntersect1pointHelp, B1';
`;;

let VerticalAnglesCong = thm `;     :: Euclid's Proposition I.15
  let A B O A' B' be point;
  assume ¬Collinear A O B                               [H1];
  assume O ∈ open (A,A')  ∧  O ∈ open (B,B')            [H2];
  thus ∡ B O A' ≡ ∡ B' O A

  proof
    ∡ A O B suppl ∡ B O A'     [AOBsupplBOA'] by H1, H2, SupplementaryAngles_DEF;
    ∡ B O A suppl ∡ A O B'     by H1, CollinearSymmetry, H2, SupplementaryAngles_DEF;
  qed     by AOBsupplBOA', -, AngleSymmetry, SupplementUnique;
`;;

let EuclidPropositionI_16 = thm `;
  let A B C D be point;
  assume ¬Collinear A B C                               [H1];
  assume C ∈ open (B,D)                                 [H2];
  thus ∡ B A C <_ang ∡ D C A

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [Distinct] by H1, NonCollinearImpliesDistinct;
    consider l such that
    Line l ∧ A ∈ l ∧ C ∈ l     [l_line] by Distinct, I1;
    consider m such that
    Line m ∧ B ∈ m ∧ C ∈ m     [m_line] by Distinct, I1;
    D ∈ m     [Dm] by m_line, H2, BetweenLinear;
    consider E such that
    E ∈ open (A,C) ∧ seg A E ≡ seg E C     [AEC] by Distinct, MidpointExists;
    ¬(A = E) ∧ ¬(E = C) ∧ Collinear A E C ∧ ¬(B = E)     [AECcol] by -, B1', H1;
    E ∈ l     [El] by l_line, AEC, BetweenLinear;
    consider F such that
    E ∈ open (B,F) ∧ seg E F ≡ seg E B     [BEF] by AECcol, SEGMENT, C1OppositeRay;
    ¬(B = E) ∧ ¬(B = F) ∧ ¬(E = F) ∧ Collinear B E F     [BEF'] by BEF, B1';
    B ∉ l     [notBl] by l_line, Distinct, I1, Collinear_DEF, H1, ∉;
    ¬Collinear A E B ∧ ¬Collinear C E B     [AEBncol] by l_line, El, AECcol, I1, Collinear_DEF, notBl, ∉;
    Angle (∡ B A E)     [angBAE] by -, CollinearSymmetry, ANGLE;
    ¬Collinear C E F     [CEFncol] by AEBncol, BEF', CollinearSymmetry, NoncollinearityExtendsToLine;
    ∡ B E A ≡ ∡ F E C     [BEAeqFEC] by AEBncol, AEC, B1', BEF, VerticalAnglesCong;
    seg E A ≡ seg E C  ∧  seg E B ≡ seg E F     by AEC, SegmentSymmetry, AECcol, BEF',  SEGMENT, BEF, C2Symmetric;
    A,E,B ≅ C,E,F     by AEBncol, CEFncol, -, BEAeqFEC, AngleSymmetry, SAS;
    ∡ B A E ≡ ∡ F C E     [BAEeqFCE] by -, TriangleCong_DEF;
    ¬Collinear E C D     [ECDncol] by AEBncol, H2, B1', CollinearSymmetry, NoncollinearityExtendsToLine;
    F ∉ l ∧ D ∉ l     [notFl] by l_line, El, Collinear_DEF, CEFncol, -, ∉;
    F ∈ ray B E ━ B  ∧  E ∉ m     by BEF, IntervalRayEZ, m_line, Collinear_DEF, AEBncol, ∉;
    F ∉ m  ∧  F,E same_side m     [Fsim_mE] by m_line, -, RaySameSide;
    ¬(B,F same_side l)  ∧  ¬(B,D same_side l)     by El, l_line, BEF, H2, SameSide_DEF;
    F,D same_side l     by l_line, notBl, notFl, -, AtMost2Sides;
    F ∈ int_angle E C D     by ECDncol, l_line, El, m_line, Dm, notFl, Fsim_mE, -, IN_InteriorAngle;
    ∡ B A E <_ang ∡ E C D     [BAElessECD] by angBAE, ECDncol, -, BAEeqFCE, AngleSymmetry, AngleOrdering_DEF;
    ray A E = ray A C  ∧  ray C E = ray C A     by AEC, B1', IntervalRay;
    ∡ B A C <_ang ∡ A C D     by BAElessECD, -, Angle_DEF;
  qed     by -, AngleSymmetry;
`;;

let ExteriorAngle = thm `;
  let A B C D be point;
  assume ¬Collinear A B C                               [H1];
  assume C ∈ open (B,D)                                 [H2];
  thus ∡ A B C <_ang ∡ A C D

  proof
    ¬(C = D) ∧ C ∈ open (D,B) ∧ Collinear B C D     [H2'] by H2, BetweenLinear, B1';
    ¬Collinear B A C ∧ ¬(A = C)     [BACncol] by H1, CollinearSymmetry, NonCollinearImpliesDistinct;
    consider E such that
    C ∈ open (A,E)     [ACE] by -, B2';
    ¬(C = E) ∧ C ∈ open (E,A) ∧ Collinear A C E     [ACE'] by -, B1';
    ¬Collinear A C D ∧ ¬Collinear D C E     [DCEncol] by H1, CollinearSymmetry, H2', -, NoncollinearityExtendsToLine;
    ∡ A B C <_ang ∡ E C B     [ABClessECB] by BACncol, ACE, EuclidPropositionI_16;
    ∡ E C B ≡ ∡ A C D     by DCEncol, ACE', H2', VerticalAnglesCong;
  qed     by ABClessECB, DCEncol, ANGLE, -, AngleTrichotomy2;
`;;

let EuclidPropositionI_17 = thm `;
  let A B C be point;
  let α β γ be point_set;
  assume ¬Collinear A B C  ∧  α = ∡ A B C  ∧  β = ∡ B C A               [H1];
  assume β suppl γ                                                      [H2];
  thus α <_ang γ

  proof
    Angle γ [angγ] by H2, SupplementImpliesAngle;
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [Distinct] by H1, NonCollinearImpliesDistinct;
    ¬Collinear B A C ∧ ¬Collinear A C B     [BACncol] by H1, CollinearSymmetry;
    consider D such that
    C ∈ open (A,D)     [ACD] by Distinct, B2';
    ∡ A B C <_ang ∡ D C B     [ABClessDCB] by BACncol, ACD, EuclidPropositionI_16;
    β suppl ∡ B C D     by -, H1, AngleSymmetry, BACncol, ACD, SupplementaryAngles_DEF;
    ∡ B C D ≡ γ     by H2, -, SupplementUnique;
  qed     by ABClessDCB, H1, AngleSymmetry, angγ, -, AngleTrichotomy2;
`;;

let EuclidPropositionI_18 = thm `;
  let A B C be point;
  assume ¬Collinear A B C                       [H1];
  assume seg A C <__ seg A B                    [H2];
  thus ∡ A B C <_ang ∡ B C A

  proof
    ¬(A = B) ∧ ¬(A = C)     [Distinct] by H1, NonCollinearImpliesDistinct;
    consider D such that
    D ∈ open (A,B) ∧ seg A C ≡ seg A D     [ADB] by Distinct, SEGMENT, H2, SegmentOrderingUse;
    ¬(D = A) ∧ ¬(D = B) ∧ D ∈ open (B,A) ∧ Collinear A D B ∧ ray B D = ray B A     [ADB'] by -, B1', IntervalRay;
    D ∈ int_angle A C B     [DintACB] by H1, CollinearSymmetry, ADB, ConverseCrossbar;
    ¬Collinear D A C ∧ ¬Collinear C B D     [DACncol] by H1, CollinearSymmetry, ADB', NoncollinearityExtendsToLine;
    seg A D ≡ seg A C     by ADB', Distinct, SEGMENT, ADB, C2Symmetric;
    ∡ C D A ≡ ∡ A C D     by DACncol, -, IsoscelesCongBaseAngles, AngleSymmetry;
    ∡ C D A <_ang ∡ A C B     [CDAlessACB] by DACncol, CollinearSymmetry, ANGLE, H1, CollinearSymmetry, DintACB, -, AngleOrdering_DEF;
    ∡ B D C suppl ∡ C D A     by DACncol, CollinearSymmetry, ADB', SupplementaryAngles_DEF;
    ∡ C B D <_ang ∡ C D A     by DACncol, -, EuclidPropositionI_17;
    ∡ C B D <_ang ∡ A C B     by -, CDAlessACB, AngleOrderTransitivity;
  qed     by -, ADB', Angle_DEF, AngleSymmetry;
`;;

let EuclidPropositionI_19 = thm `;
  let A B C be point;
  assume ¬Collinear A B C                       [H1];
  assume ∡ A B C <_ang ∡ B C A                 [H2];
  thus seg A C  <__ seg A B

  proof
    ¬Collinear B A C ∧ ¬Collinear B C A ∧ ¬Collinear A C B     [BACncol] by H1, CollinearSymmetry;
    ¬(A = B) ∧ ¬(A = C)     [Distinct] by H1, NonCollinearImpliesDistinct;
    assume ¬(seg A C  <__ seg A B);
    seg A B ≡ seg A C   ∨  seg A B  <__ seg A C     by Distinct, SEGMENT, -, SegmentTrichotomy;
    cases by -;
    suppose seg A B ≡ seg A C;
      ∡ C B A ≡ ∡ B C A     by BACncol, -, IsoscelesCongBaseAngles;
    qed     by -, AngleSymmetry, H2, AngleTrichotomy1;
    suppose seg A B  <__ seg A C;
      ∡ A C B <_ang ∡ C B A     by BACncol, -, EuclidPropositionI_18;
    qed     by H1, BACncol, ANGLE, -, AngleSymmetry, H2, AngleTrichotomy;
  end;
`;;

let EuclidPropositionI_20 = thm `;
  let A B C D be point;
  assume ¬Collinear A B C                               [H1];
  assume A ∈ open (B,D)  ∧  seg A D ≡ seg A C           [H2];
  thus seg B C <__ seg B D

  proof
    ¬(B = D) ∧ ¬(A = D) ∧ A ∈ open (D,B) ∧ Collinear B A D ∧ ray D A = ray D B     [BAD'] by H2, B1', IntervalRay;
    ¬Collinear C A D     [CADncol] by H1, CollinearSymmetry, BAD', NoncollinearityExtendsToLine;
    ¬Collinear D C B ∧ ¬Collinear B D C     [DCBncol] by H1, CollinearSymmetry, BAD', NoncollinearityExtendsToLine; ::  13
    Angle (∡ C D A)     [angCDA] by CADncol, CollinearSymmetry, ANGLE;
    ∡ C D A ≡ ∡ D C A     [CDAeqDCA] by CADncol, CollinearSymmetry, H2, IsoscelesCongBaseAngles;
    A ∈ int_angle D C B     by DCBncol, BAD', ConverseCrossbar;
    ∡ C D A <_ang ∡ D C B     by angCDA, DCBncol, -, CDAeqDCA, AngleOrdering_DEF;
    ∡ B D C <_ang ∡ D C B     by -, BAD', Angle_DEF, AngleSymmetry;
  qed     by DCBncol, -, EuclidPropositionI_19;
`;;

let EuclidPropositionI_21 = thm `;
  let A B C D be point;
  assume ¬Collinear A B C                       [H1];
  assume D ∈ int_triangle A B C                 [H2];
  thus ∡ A B C <_ang ∡ C D A

  proof
    ¬(B = A) ∧ ¬(B = C) ∧ ¬(A = C)     [Distinct] by H1, NonCollinearImpliesDistinct;
    D ∈ int_angle B A C  ∧  D ∈ int_angle C B A     [DintTri] by H2, IN_InteriorTriangle, InteriorAngleSymmetry;
    consider E such that
    E ∈ open (B,C) ∧ E ∈ ray A D ━ A     [BEC] by -, Crossbar_THM;
    ¬(B = E) ∧ ¬(E = C) ∧ Collinear B E C  ∧  Collinear A D E      [BEC'] by -, B1', IN_DELETE, IN_Ray;
    ray B E = ray B C  ∧  E ∈ ray B C ━ B     [rBErBC] by BEC, IntervalRay, IntervalRayEZ;
    D ∈ int_angle A B E     [DintABE] by DintTri, -, InteriorAngleSymmetry, InteriorWellDefined;
    D ∈ open (A,E)     [ADE] by BEC', -, AlternateConverseCrossbar;
    ray E D = ray E A     [rEDrEA] by -, B1', IntervalRay;
    ¬Collinear A B E ∧ ¬Collinear B E A  ∧ ¬Collinear C B D ∧ ¬(A = D)     [ABEncol] by DintABE, IN_InteriorAngle, CollinearSymmetry, DintTri, InteriorEZHelp;
    ¬Collinear E D C ∧ ¬Collinear C E D     [EDCncol] by -, CollinearSymmetry, BEC',  NoncollinearityExtendsToLine;
    ∡ A B E <_ang ∡ A E C     by ABEncol, BEC, ExteriorAngle;
    ∡ A B C <_ang ∡ C E D     [ABClessAEC] by -, rBErBC, rEDrEA, Angle_DEF, AngleSymmetry;
    ∡ C E D  <_ang  ∡ C D A     by EDCncol, ADE, B1', ExteriorAngle;
  qed     by ABClessAEC, -, AngleOrderTransitivity;
`;;

let AngleTrichotomy3 = thm `;
  let α β γ be point_set;
  assume α <_ang β  ∧  Angle γ  ∧  γ ≡ α                  [H1];
  thus γ <_ang β

  proof
    consider A O B G such that
    Angle α ∧ ¬Collinear A O B ∧ β = ∡ A O B ∧ G ∈ int_angle A O B ∧ α ≡ ∡ A O G     [H1'] by H1, AngleOrdering_DEF;
    ¬Collinear A O G     by -, InteriorEZHelp;
    γ ≡ ∡ A O G     by H1, H1', -, ANGLE, C5Transitive;
  qed     by H1, H1', -, AngleOrdering_DEF;
`;;

let InteriorCircleConvexHelp = thm `;
  let O A B C be point;
  assume ¬Collinear A O C                               [H1];
  assume B ∈ open (A,C)                                 [H2];
  assume seg O A <__ seg O C  ∨  seg O A ≡ seg O C      [H3];
  thus seg O B <__ seg O C

  proof
    ¬Collinear O C A ∧ ¬Collinear C O A ∧ ¬(O = A) ∧ ¬(O = C)     [H1'] by H1, CollinearSymmetry, NonCollinearImpliesDistinct;
    ray A B = ray A C  ∧  ray C B = ray C A     [equal_rays] by H2, IntervalRay, B1';
    ∡ O C A <_ang ∡ C A O  ∨  ∡ O C A ≡ ∡ C A O
    proof
      cases by H3;
      suppose seg O A <__ seg O C;
      qed     by H1', -, EuclidPropositionI_18;
      suppose seg O A ≡ seg O C [seg_eq];
        seg O C ≡ seg O A     by H1', SEGMENT, -, C2Symmetric;
      qed     by H1', -, IsoscelesCongBaseAngles, AngleSymmetry;
    end;
    ∡ O C B <_ang ∡ B A O  ∨  ∡ O C B ≡ ∡ B A O     by -, equal_rays, Angle_DEF;
    ∡ B C O <_ang ∡ O A B  ∨  ∡ B C O ≡ ∡ O A B     [BCOlessOAB] by -, AngleSymmetry;
    ¬Collinear O A B ∧ ¬Collinear B C O ∧ ¬Collinear O C B     [OABncol] by H1, CollinearSymmetry, H2, B1', NoncollinearityExtendsToLine;
    ∡ O A B <_ang ∡ O B C     by -, H2, ExteriorAngle;
    ∡ B C O <_ang ∡ O B C by BCOlessOAB, -, AngleOrderTransitivity, OABncol, ANGLE, -, AngleTrichotomy3;
  qed     by OABncol, -, AngleSymmetry, EuclidPropositionI_19;
`;;

let InteriorCircleConvex = thm `;
  let O R A B C be point;
  assume  ¬(O = R)                                      [H1];
  assume B ∈ open (A,C)                                 [H2];
  assume A ∈ int_circle O R  ∧  C ∈ int_circle O R      [H3];
  thus B ∈ int_circle O R

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ B ∈ open (C,A)     [H2'] by H2, B1';
    (A = O  ∨  seg O A <__ seg O R)  ∧  (C = O  ∨  seg O C <__ seg O R)     [ACintOR] by H3, H1, IN_InteriorCircle;
    cases;
    suppose O = A ∨ O = C;
      B ∈ open (O,C)  ∨  B ∈ open (O,A)     by -, H2, B1';
      seg O B <__ seg O A ∧ ¬(O = A)  ∨  seg O B <__ seg O C ∧ ¬(O = C)     by -, B1', SEGMENT, C2Reflexive,  SegmentOrdering_DEF;
      seg O B <__ seg O R     by -, ACintOR, SegmentOrderTransitivity;
    qed by -, H1, IN_InteriorCircle;
    suppose ¬(O = A) ∧ ¬(O = C)     [OnotAC];
      cases;
      suppose ¬Collinear A O C     [AOCncol];
        seg O A <__ seg O C  ∨  seg O A ≡ seg O C  ∨  seg O C <__ seg O A     by OnotAC, SEGMENT,  SegmentTrichotomy;
        seg O B <__ seg O C  ∨  seg O B <__ seg O A     by AOCncol, H2, -, InteriorCircleConvexHelp, CollinearSymmetry, B1';
      qed     by OnotAC, ACintOR, -, SegmentOrderTransitivity, H1, IN_InteriorCircle;
      suppose Collinear A O C                           [AOCcol];
        consider l such that
        Line l ∧ A ∈ l ∧ C ∈ l     by H2', I1;
        Collinear B A O ∧ Collinear B C O     [OABCcol] by -, H2, BetweenLinear, H2', AOCcol, CollinearLinear, Collinear_DEF;
        B ∉ open (O,A) ∧ B ∉ open (O,C)  ⇒  B = O
        proof
          assume B ∉ open (O,A) ∧ B ∉ open (O,C);
          O ∈ ray B A ∩ ray B C     by H2', OABCcol, -, IN_Ray, IN_INTER;
        qed     by -, H2, OppositeRaysIntersect1point, IN_SING;
        B ∈ open (O,A)  ∨  B ∈ open (O,C)  ∨  B = O     by -, ∉;
        seg O B <__ seg O A  ∨  seg O B <__ seg O C  ∨  B = O     by -, B1', SEGMENT, C2Reflexive,  SegmentOrdering_DEF;
        seg O B <__ seg O R  ∨  B = O     by -, ACintOR, OnotAC, SegmentOrderTransitivity;
      qed     by -, H1, IN_InteriorCircle;
    end;
  end;
`;;

let SegmentTrichotomy3 = thm `;
  let s t u be point_set;
  assume s <__ t  ∧  Segment u  ∧  u ≡ s                [H1];
  thus u <__ t

  proof
    consider C D X such that
    Segment s ∧ t = seg C D ∧ X ∈ open (C,D) ∧ s ≡ seg C X ∧ ¬(C = X)     [H1'] by H1, SegmentOrdering_DEF, B1';
    u ≡ seg C X     by H1, -, SEGMENT, C2Transitive;
  qed     by H1, H1', -, SegmentOrdering_DEF;
`;;

let EuclidPropositionI_24Help = thm `;
  let O A C O' D F be point;
  assume ¬Collinear A O C ∧ ¬Collinear D O' F                   [H1];
  assume seg O' D ≡ seg O A  ∧  seg O' F ≡ seg O C              [H2];
  assume  ∡ D O' F <_ang ∡ A O C                                [H3];
  assume seg O A <__ seg O C  ∨  seg O A ≡ seg O C              [H4];
  thus seg D F <__ seg A C

  proof
    consider K such that
    K ∈ int_angle A O C ∧ ∡ D O' F ≡ ∡ A O K     [KintAOC] by H1, ANGLE, H3, AngleOrderingUse;
    ¬(O = C) ∧ ¬(D = F) ∧ ¬(O' = F) ∧ ¬(O = K)     [Distinct] by H1, NonCollinearImpliesDistinct, -, InteriorEZHelp;
    consider B such that
    B ∈ ray O K ━ O  ∧  seg O B ≡ seg O C     [BrOK] by Distinct, SEGMENT, -, C1;
    ray O B = ray O K     by Distinct, -, RayWellDefined;
    ∡ D O' F ≡ ∡ A O B     [DO'FeqAOB] by KintAOC, -, Angle_DEF;
    B ∈ int_angle A O C     [BintAOC] by KintAOC, BrOK, WholeRayInterior;
    ¬(B = O) ∧ ¬Collinear A O B     [AOBncol] by -, InteriorEZHelp;
    seg O C ≡ seg O B     [OCeqOB] by Distinct, -, SEGMENT, BrOK, C2Symmetric;
    seg O' F ≡ seg O B     by Distinct, SEGMENT, AOBncol, H2, -, C2Transitive;
    D,O',F ≅ A,O,B     by H1, AOBncol, H2, -, DO'FeqAOB, SAS;
    seg D F ≡ seg A B     [DFeqAB] by -, TriangleCong_DEF;
    consider G such that
    G ∈ open (A,C)  ∧  G ∈ ray O B ━ O  ∧  ¬(G = O)     [AGC] by BintAOC, Crossbar_THM, B1', IN_DELETE;
    Segment (seg O G) ∧ ¬(O = B)     [notOB] by AGC, SEGMENT, BrOK, IN_DELETE;
    seg O G <__ seg O C     by H1, AGC, H4, InteriorCircleConvexHelp;
    seg O G <__ seg O B     by -, OCeqOB, BrOK, IN_DELETE, SEGMENT, SegmentTrichotomy2;
    consider G' such that
    G' ∈ open (O,B)  ∧  seg O G ≡ seg O G'     [OG'B] by notOB, -, SegmentOrderingUse;
    ¬(G' = O)  ∧  seg O G' ≡ seg O G'  ∧  Segment (seg O G')     [notG'O] by -, B1', SEGMENT, C2Reflexive, SEGMENT;
    G' ∈ ray O B ━ O     by OG'B, IntervalRayEZ;
    G' = G  ∧  G ∈ open (B,O)     by notG'O, notOB, -, AGC, OG'B, C1, B1';
    ConvexQuadrilateral B A O C     by H1, -, AGC, DiagonalsIntersectImpliesConvexQuad;
    A ∈ int_angle O C B  ∧  O ∈ int_angle C B A  ∧  Quadrilateral B A O C     [OintCBA] by -, ConvexQuad_DEF;
    A ∈ int_angle B C O     [AintBCO] by -, InteriorAngleSymmetry;
    Tetralateral B A O C     by OintCBA, Quadrilateral_DEF;
    ¬Collinear C B A  ∧ ¬Collinear B C O ∧ ¬Collinear C O B ∧ ¬Collinear C B O     [BCOncol] by -, Tetralateral_DEF, CollinearSymmetry;
    ∡ B C O ≡ ∡ C B O     [BCOeqCBO] by -, OCeqOB, IsoscelesCongBaseAngles;
    ¬Collinear B C A ∧ ¬Collinear A C B     [ACBncol] by AintBCO, InteriorEZHelp, CollinearSymmetry;
    ∡ B C A ≡ ∡ B C A  ∧  Angle (∡ B C A)  ∧  ∡ C B O ≡ ∡ C B O     [CBOref] by -, ANGLE, BCOncol, C5Reflexive;
    ∡ B C A <_ang ∡ B C O     by -, BCOncol, ANGLE, AintBCO, AngleOrdering_DEF;
    ∡ B C A <_ang ∡ C B O     [BCAlessCBO] by -, BCOncol, ANGLE, BCOeqCBO, AngleTrichotomy2;
    ∡ C B O <_ang ∡ C B A     by BCOncol, ANGLE, OintCBA, CBOref, AngleOrdering_DEF;
    ∡ A C B <_ang ∡ C B A     by BCAlessCBO, -, AngleOrderTransitivity, AngleSymmetry;
    seg A B <__ seg A C     by ACBncol, -, EuclidPropositionI_19;
 qed     by -, Distinct, SEGMENT, DFeqAB, SegmentTrichotomy3;
`;;

let EuclidPropositionI_24 = thm `;
  let O A C O' D F be point;
  assume ¬Collinear A O C ∧ ¬Collinear D O' F                   [H1];
  assume seg O' D ≡ seg O A ∧ seg O' F ≡ seg O C                [H2];
  assume  ∡ D O' F <_ang ∡ A O C                                [H3];
  thus seg D F <__ seg A C

  proof
    ¬(O = A) ∧ ¬(O = C) ∧ ¬Collinear C O A ∧ ¬Collinear F O' D     [Distinct] by H1, NonCollinearImpliesDistinct, CollinearSymmetry;
    seg O A ≡ seg O C  ∨  seg O A <__ seg O C  ∨  seg O C <__ seg O A     by  -, SEGMENT, SegmentTrichotomy;
    cases by -;
      suppose seg O A <__ seg O C  ∨  seg O A ≡ seg O C;
      qed     by H1, H2, H3, -, EuclidPropositionI_24Help;
      suppose seg O C <__ seg O A     [H4];
        ∡ F O' D <_ang ∡ C O A     by H3, AngleSymmetry;
     qed     by Distinct, H3, AngleSymmetry, H2, H4, EuclidPropositionI_24Help, SegmentSymmetry;
  end;
`;;

let EuclidPropositionI_25 = thm `;
  let O A C O' D F be point;
  assume ¬Collinear A O C ∧ ¬Collinear D O' F                   [H1];
  assume seg O' D ≡ seg O A ∧ seg O' F ≡ seg O C                [H2];
  assume  seg D F <__ seg A C                                   [H3];
  thus ∡ D O' F <_ang ∡ A O C

  proof
    ¬(O = A) ∧ ¬(O = C) ∧ ¬(A = C) ∧ ¬(D = F) ∧ ¬(O' = D) ∧ ¬(O' = F)     [Distinct] by H1, NonCollinearImpliesDistinct;
    assume ¬(∡ D O' F <_ang ∡ A O C);
    ∡ D O' F ≡ ∡ A O C  ∨  ∡ A O C <_ang ∡ D O' F     by H1, ANGLE, -, AngleTrichotomy;
    cases by -;
    suppose ∡ D O' F ≡ ∡ A O C;
      D,O',F ≅ A,O,C     by H1, H2, -, SAS;
      seg D F ≡ seg A C     by -, TriangleCong_DEF;
    qed     by Distinct, SEGMENT, -, H3, SegmentTrichotomy;
    suppose ∡ A O C <_ang ∡ D O' F [Con];
      seg O A ≡ seg O' D  ∧  seg O C  ≡ seg O' F     [H2'] by Distinct, SEGMENT, H2, C2Symmetric;
      seg A C <__ seg D F     by H1, -, Con, EuclidPropositionI_24;
    qed      by Distinct, SEGMENT, -, H3, SegmentTrichotomy;
  end;
`;;

let AAS = thm `;
  let A B C A' B' C' be point;
  assume ¬Collinear A B C ∧ ¬Collinear A' B' C'                 [H1];
  assume ∡ A B C ≡ ∡ A' B' C'  ∧  ∡ B C A ≡ ∡ B' C' A'          [H2];
  assume seg A B ≡ seg A' B'                                            [H3];
  thus A,B,C ≅ A',B',C'

  proof
    ¬(A = B) ∧ ¬(B = C) ∧ ¬(B' = C')     [Distinct] by H1, NonCollinearImpliesDistinct;
    consider G such that
    G ∈ ray B C ━ B ∧ seg B G ≡ seg B' C'     [Gexists] by Distinct, SEGMENT, C1;
    ¬(G = B)  ∧  B ∉ open (G,C)  ∧ Collinear G B C     [notGBC] by -, IN_DELETE, IN_Ray, CollinearSymmetry;
    ¬Collinear A B G ∧ ¬Collinear B G A     [ABGncol] by H1, notGBC, CollinearSymmetry, NoncollinearityExtendsToLine;
    ray B G = ray B C     by Distinct, Gexists, RayWellDefined;
    ∡ A B G = ∡ A B C     by Distinct, -, Angle_DEF;
    A,B,G ≅ A',B',C'     [ABG≅A'B'C'] by H1, ABGncol, H3, SegmentSymmetry, H2, -, Gexists, SAS;
    ∡ B G A ≡ ∡ B' C' A'     [BGAeqB'C'A'] by -, TriangleCong_DEF;
    ¬Collinear B C A  ∧ ¬Collinear B' C' A'     [BCAncol] by H1, CollinearSymmetry;
    ∡ B' C' A' ≡ ∡ B C A  ∧  ∡ B C A ≡ ∡ B C A     [BCArefl] by -, ANGLE, H2, C5Symmetric, C5Reflexive;
    ∡ B G A ≡ ∡ B C A     [BGAeqBCA] by ABGncol, BCAncol, ANGLE, BGAeqB'C'A', -, C5Transitive;
    cases;
    suppose G = C;
    qed     by -, ABG≅A'B'C';
    suppose ¬(G = C)     [notGC];
     ¬Collinear A C G ∧ ¬Collinear A G C     [ACGncol] by H1, notGBC, -, CollinearSymmetry, NoncollinearityExtendsToLine;
      C ∈ open (B,G) ∨ G ∈ open (C,B)     by notGBC, notGC, Distinct, B3', ∉;
      cases     by -;
      suppose C ∈ open (B,G) ;
        C ∈ open (G,B)  ∧ ray G C = ray G B     [rGCrBG] by -, B1', IntervalRay;
        ∡ A G C <_ang ∡ A C B     by ACGncol, -, ExteriorAngle;
        ∡ B G A <_ang ∡ B C A     by -, rGCrBG, Angle_DEF, AngleSymmetry, AngleSymmetry;
      qed     by ABGncol, BCAncol, ANGLE, -, AngleSymmetry, BGAeqBCA, AngleTrichotomy;
      suppose G ∈ open (C,B)     [CGB];
        ray C G = ray C B  ∧  ∡ A C G <_ang ∡ A G B     by -, IntervalRay, ACGncol, ExteriorAngle;
        ∡ A C B <_ang ∡ B G A     by -, Angle_DEF, AngleSymmetry;
        ∡ B C A <_ang ∡ B C A     by -, BCAncol, ANGLE, BGAeqBCA, AngleTrichotomy2, AngleSymmetry;
      qed     by -, BCArefl, AngleTrichotomy1;
    end;
  end;
`;;

let ParallelSymmetry = thm `;
  ∀ l k: point_set. l ∥ k  ⇒  k ∥ l
  by PARALLEL, INTER_COMM;
`;;

let AlternateInteriorAngles = thm `;
  let A B C E be point;
  let l m t be point_set;
  assume Line l ∧ A ∈ l ∧ E ∈ l                                   [l_line];
  assume Line m ∧ B ∈ m ∧ C ∈ m                                   [m_line];
  assume Line t ∧ A ∈ t ∧ B ∈ t                                   [t_line];
  assume ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t           [Distinct];
  assume ¬(C,E same_side t)                                        [Cnsim_tE];
  assume ∡ E A B ≡ ∡ C B A [AltIntAngCong];
  thus l ∥ m

  proof
    ¬Collinear E A B ∧ ¬Collinear C B A     [EABncol] by t_line, Distinct, I1, Collinear_DEF, ∉;
    B ∉ l ∧ A ∉ m     [notAmBl] by l_line, m_line, Collinear_DEF, -, ∉;
    assume ¬(l ∥ m);
    ¬(l ∩ m = ∅)     by -, l_line, m_line, PARALLEL;
    consider G such that
    G ∈ l ∧ G ∈ m     [Glm] by -, MEMBER_NOT_EMPTY, IN_INTER;
    ¬(G = A) ∧ ¬(G = B) ∧ Collinear B G C ∧ Collinear B C G ∧ Collinear A E G ∧ Collinear A G E     [GnotAB] by -, notAmBl, ∉, m_line, l_line, Collinear_DEF;
    ¬Collinear A G B ∧ ¬Collinear B G A ∧ G ∉ t      [AGBncol]  by EABncol, CollinearSymmetry, -, NoncollinearityExtendsToLine, t_line, Collinear_DEF, ∉;
    ¬(E,C same_side t)     [Ensim_tC] by t_line, -, Distinct, Cnsim_tE, SameSideSymmetric;
    C ∈ m ━ B  ∧  G ∈ m ━ B     [CGm_B] by m_line, Glm, Distinct, GnotAB, IN_DELETE;
    E ∈ l ━ A  ∧  G ∈ l ━ A     [EGm_A] by l_line, Glm, Distinct, GnotAB, IN_DELETE;
    ¬(G,E same_side t)
    proof
      assume G,E same_side t     [Gsim_tE];
      A ∉ open (G,E)     [notGAE] by t_line, -, SameSide_DEF, ∉;
      G ∈ ray A E ━ A     by Distinct, GnotAB, notGAE, IN_Ray, GnotAB, IN_DELETE;
      ray A G = ray A E     [rAGrAE] by Distinct, -, RayWellDefined;
      ¬(C,G same_side t)     by t_line, AGBncol, Distinct, Gsim_tE, Cnsim_tE, SameSideTransitive;
       C ∉ ray B G  ∧  B ∈ open (C,G)     by t_line, AGBncol, Distinct, -, RaySameSide, ∉, GnotAB, IN_DELETE, IN_Ray;
      ∡ G A B <_ang ∡ C B A     by AGBncol, -, B1', EuclidPropositionI_16;
      ∡ E A B <_ang ∡ C B A     by -, rAGrAE, Angle_DEF;
    qed     by EABncol, ANGLE, AltIntAngCong, -, AngleTrichotomy1;
    G,C same_side t     [Gsim_tC] by t_line, AGBncol, Distinct, -, Cnsim_tE, AtMost2Sides;
    :: now we make a symmetric argument
    B ∉ open (G,C)     [notGBC] by t_line, -, SameSide_DEF, ∉;
    G ∈ ray B C ━ B     by Distinct, GnotAB, notGBC, IN_Ray, GnotAB, IN_DELETE;
    ray B G = ray B C     [rBGrBC] by Distinct, -, RayWellDefined;
    ∡ C B A ≡ ∡ E A B     [flipAltIntAngCong] by EABncol, ANGLE, AltIntAngCong, C5Symmetric;
    ¬(E,G same_side t)     by t_line, AGBncol, Distinct, Gsim_tC, Ensim_tC, SameSideTransitive;
    E ∉ ray A G   ∧  A ∈ open (E,G)     by t_line, AGBncol, Distinct, -, RaySameSide, ∉, GnotAB, IN_Ray, IN_DELETE;
    ∡ G B A <_ang ∡ E A B     by AGBncol, -, B1', EuclidPropositionI_16;
    ∡ C B A <_ang ∡ E A B     by -, rBGrBC, Angle_DEF;
  qed     by EABncol, ANGLE, flipAltIntAngCong, -, AngleTrichotomy1;
`;;

let EuclidPropositionI_28 = thm `;
  let A B C D E F G H be point;
  let l m t be point_set;
  assume Line l ∧ A ∈ l ∧ B ∈ l ∧ G ∈ l                 [l_line];
  assume Line m ∧ C ∈ m ∧ D ∈ m ∧ H ∈ m                 [m_line];
  assume Line t ∧ G ∈ t ∧ H ∈ t                         [t_line];
  assume  G ∉ m ∧ H ∉ l                                 [notGmHl];
  assume G ∈ open (A,B)  ∧ H ∈ open (C,D)                       [H1];
  assume G ∈ open (E,H)  ∧  H ∈ open (F,G)                      [H2];
  assume ¬(D,A same_side t)                                     [H3];
  assume ∡ E G B ≡ ∡ G H D  ∨  ∡ B G H suppl ∡ G H D            [H4];
  thus l ∥ m

  proof
    ¬(A = G) ∧ ¬(G = B) ∧ ¬(H = D) ∧ ¬(E = G) ∧ ¬(G = H) ∧ Collinear A G B ∧ Collinear E G H     [Distinct] by H1, H2, B1';
    ¬Collinear H G A ∧ ¬Collinear G H D ∧ A ∉ t ∧ D ∉ t     [HGAncol] by l_line, m_line, Distinct, I1, Collinear_DEF, notGmHl, ∉, t_line, Collinear_DEF;
    ¬Collinear B G H ∧ ¬Collinear A G E ∧ ¬Collinear E G B     [BGHncol] by -, Distinct, CollinearSymmetry, NoncollinearityExtendsToLine;
    ∡ A G H ≡ ∡ D H G
    proof
      cases     by H4;
      suppose ∡ E G B ≡ ∡ G H D     [EGBeqGHD];
        ∡ E G B ≡ ∡ H G A     by BGHncol, H1, H2, VerticalAnglesCong;
        ∡ H G A ≡ ∡ E G B     by BGHncol, HGAncol, ANGLE, -, C5Symmetric;
        ∡ H G A ≡ ∡ G H D     by BGHncol, HGAncol, ANGLE, -, EGBeqGHD, C5Transitive;
      qed     by -, AngleSymmetry;
      suppose ∡ B G H suppl ∡ G H D [BGHeqGHD];
        ∡ B G H suppl ∡ H G A     by BGHncol, H1, B1', SupplementaryAngles_DEF;
      qed     by -, BGHeqGHD, AngleSymmetry, SupplementUnique, AngleSymmetry;
    end;
  qed     by l_line, m_line, t_line, Distinct, HGAncol, H3, -,  AlternateInteriorAngles;
`;;

let OppositeSidesCongImpliesParallelogram = thm `;
  let A B C D be point;
  assume Quadrilateral A B C D                          [H1];
  assume seg A B ≡ seg C D  ∧  seg B C ≡ seg D A        [H2];
  thus Parallelogram A B C D

  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     [TetraABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
    consider a c such that
    Line a ∧ A ∈ a ∧ B ∈ a   ∧
    Line c ∧ C ∈ c ∧ D ∈ c     [ac_line] by TetraABCD, I1;
    consider b d such that
    Line b ∧ B ∈ b ∧ C ∈ b   ∧
    Line d ∧ D ∈ d ∧ A ∈ d     [bd_line] by TetraABCD, I1;
    consider l such that
    Line l ∧ A ∈ l ∧ C ∈ l     [l_line] by TetraABCD, I1;
    consider m such that
    Line m ∧ B ∈ m ∧ D ∈ m     [m_line] by TetraABCD, I1;
    B ∉ l ∧ D ∉ l ∧ A ∉ m  ∧ C ∉ m     [notBDlACm] by l_line, m_line, TetraABCD, Collinear_DEF, ∉;
    seg A C ≡ seg C A  ∧  seg B D ≡ seg D B     [seg_refl] by TetraABCD, SEGMENT, C2Reflexive, SegmentSymmetry;
    A,B,C ≅ C,D,A     by TetraABCD, H2, -, SSS;
    ∡ B C A ≡ ∡ D A C  ∧  ∡ C A B ≡ ∡ A C D     [BCAeqDAC] by -, TriangleCong_DEF;
    seg C D ≡ seg A B     [CDeqAB] by TetraABCD, SEGMENT, H2, C2Symmetric;
    B,C,D ≅ D,A,B     by TetraABCD, H2, -, seg_refl, SSS;
    ∡ C D B ≡ ∡ A B D  ∧  ∡ D B C ≡ ∡ B D A     [CDBeqABD] by -, TriangleCong_DEF;
    ¬(B,D same_side l)  ∨  ¬(A,C same_side m)     by H1, l_line, m_line, FiveChoicesQuadrilateral;
    cases     by -;
    suppose ¬(B,D same_side l);
      ¬(D,B same_side l)     by l_line, notBDlACm, -, SameSideSymmetric;
      a ∥ c  ∧  b ∥ d     by ac_line, l_line, TetraABCD, notBDlACm, -, BCAeqDAC, AngleSymmetry, AlternateInteriorAngles, bd_line, BCAeqDAC;
    qed     by H1, ac_line, bd_line, -, Parallelogram_DEF;
    suppose ¬(A,C same_side m);
      b ∥ d  ∧  c ∥ a     by bd_line, m_line, TetraABCD, notBDlACm, -, CDBeqABD, AngleSymmetry, AlternateInteriorAngles, ac_line, CDBeqABD;
    qed     by H1, ac_line, bd_line, -, ParallelSymmetry, Parallelogram_DEF;
  end;
`;;

let OppositeAnglesCongImpliesParallelogramHelp = thm `;
  let A B C D be point;
  let a c be point_set;
  assume Quadrilateral A B C D                          [H1];
  assume ∡ A B C ≡ ∡ C D A  ∧  ∡ D A B ≡ ∡ B C D        [H2];
  assume Line a ∧ A ∈ a ∧ B ∈ a                 [a_line];
  assume Line c  ∧ C ∈ c ∧ D ∈ c                        [c_line];
  thus a ∥ c

  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     [TetraABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
    ∡ C D A ≡ ∡ A B C  ∧  ∡ B C D ≡ ∡ D A B     [H2'] by TetraABCD, ANGLE, H2, C5Symmetric;
    consider l m such that
    Line l ∧ A ∈ l ∧ C ∈ l  ∧
    Line m ∧ B ∈ m ∧ D ∈ m     [lm_line] by TetraABCD, I1;
    consider b d such that
    Line b ∧ B ∈ b ∧ C ∈ b   ∧  Line d ∧ D ∈ d ∧ A ∈ d     [bd_line] by TetraABCD, I1;
    A ∉ c ∧ B ∉ c ∧ A ∉ b ∧ D ∉ b ∧ B ∉ d ∧ C ∉ d     [point_off_line] by c_line, bd_line, Collinear_DEF, TetraABCD, ∉;
    ¬(A ∈ int_triangle B C D  ∨  B ∈ int_triangle C D A  ∨
    C ∈ int_triangle D A B  ∨  D ∈ int_triangle A B C)
    proof
      assume A ∈ int_triangle B C D  ∨  B ∈ int_triangle C D A  ∨
      C ∈ int_triangle D A B  ∨  D ∈ int_triangle A B C;
      ∡ B C D <_ang ∡ D A B  ∨  ∡ C D A <_ang ∡ A B C  ∨
      ∡ D A B <_ang ∡ B C D  ∨  ∡ A B C <_ang ∡ C D A     by TetraABCD, -, EuclidPropositionI_21;
    qed     by -, H2', H2, AngleTrichotomy1;
    ConvexQuadrilateral A B C D     by H1, lm_line, -, FiveChoicesQuadrilateral;
    A ∈ int_angle B C D  ∧  B ∈ int_angle C D A  ∧
    C ∈ int_angle D A B  ∧  D ∈ int_angle A B C     [AintBCD] by -, ConvexQuad_DEF;
    B,A same_side c  ∧  B,C same_side d     [Bsim_cA] by c_line, bd_line, -, InteriorUse;
    A,D same_side b     [Asim_bD] by bd_line, c_line, AintBCD, InteriorUse;
    assume ¬(a ∥ c);
    consider G such that
    G ∈ a ∧ G ∈ c     [Gac] by -, a_line, c_line, PARALLEL, MEMBER_NOT_EMPTY, IN_INTER;
    Collinear A B G ∧ Collinear D G C ∧ Collinear C G D     [ABGcol] by a_line, -, Collinear_DEF, c_line;
    ¬(G = A) ∧ ¬(G = B) ∧ ¬(G = C) ∧ ¬(G = D)     [GnotABCD] by Gac, ABGcol, TetraABCD, CollinearSymmetry, Collinear_DEF;
    ¬Collinear B G C ∧ ¬Collinear A D G     [BGCncol] by c_line, Gac, GnotABCD, I1, Collinear_DEF, point_off_line, ∉;
    ¬Collinear B C G ∧ ¬Collinear G B C ∧ ¬Collinear G A D ∧ ¬Collinear A G D     [BCGncol] by -, CollinearSymmetry;
    G ∉ b ∧ G ∉ d     [notGb] by bd_line, Collinear_DEF, BGCncol, ∉;
    G ∉ open (B,A)     [notBGA] by Bsim_cA, Gac, SameSide_DEF, ∉;
    B ∉ open (A,G)     [notABG]
    proof
      assume ¬(B ∉ open (A,G));
      B ∈ open (A,G)     [ABG] by -, ∉;
      ray A B = ray A G     [rABrAG] by -, IntervalRay;
      ¬(A,G same_side b)     by bd_line, ABG, SameSide_DEF;
      ¬(D,G same_side b)     by bd_line, point_off_line, notGb, Asim_bD, -, SameSideTransitive;
      D ∉ ray C G     by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, ∉;
      C ∈ open (D,G)     [DCG] by GnotABCD, ABGcol, -, IN_Ray, ∉;
      consider M such that
      D ∈ open (C,M)     [CDM] by TetraABCD, B2';
      D ∈ open (G,M)     [GDM] by -, B1', DCG, TransitivityBetweennessHelp;
      ∡ C D A suppl ∡ A D M  ∧  ∡ A B C suppl ∡ C B G     by TetraABCD, CDM, ABG, SupplementaryAngles_DEF;
      ∡ M D A ≡ ∡ G B C     [MDAeqGBC] by -, H2', SupplementsCongAnglesCong, AngleSymmetry;
      ∡ G A D <_ang ∡ M D A  ∧  ∡ G B C <_ang ∡ D C B     by BCGncol, BGCncol, GDM, DCG, B1', EuclidPropositionI_16;
      ∡ G A D <_ang ∡ D C B     by  -, BCGncol, ANGLE, MDAeqGBC, AngleTrichotomy2, AngleOrderTransitivity;
      ∡ D A B <_ang ∡ B C D     by -, rABrAG, Angle_DEF, AngleSymmetry;
    qed     by -, H2, AngleTrichotomy1;
    A ∉ open (G,B)
    proof
      assume ¬(A ∉ open (G,B));
      A ∈ open (B,G)     [BAG] by -, B1', ∉;
      ray B A = ray B G     [rBArBG] by -, IntervalRay;
      ¬(B,G same_side d)     by bd_line, BAG, SameSide_DEF;
      ¬(C,G same_side d)     by bd_line, point_off_line, notGb, Bsim_cA, -,  SameSideTransitive;
      C ∉ ray D G     by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, ∉;
      D ∈ open (C,G)     [CDG] by GnotABCD, ABGcol, -, IN_Ray, ∉;
      consider M such that
      C ∈ open (D,M)     [DCM] by B2', TetraABCD;
      C ∈ open (G,M)     [GCM] by -, B1', CDG, TransitivityBetweennessHelp;
      ∡ B C D suppl ∡ M C B  ∧  ∡ D A B suppl ∡ G A D     by TetraABCD, CollinearSymmetry, DCM, BAG, SupplementaryAngles_DEF, AngleSymmetry;
      ∡ M C B ≡ ∡ G A D     [GADeqMCB] by -, H2', SupplementsCongAnglesCong;
      ∡ G B C <_ang ∡ M C B  ∧  ∡ G A D <_ang ∡ C D A     by BGCncol, GCM, BCGncol, CDG, B1', EuclidPropositionI_16;
      ∡ G B C <_ang ∡ C D A     by -, BCGncol, ANGLE, GADeqMCB, AngleTrichotomy2, AngleOrderTransitivity;
      ∡ A B C <_ang ∡ C D A     by -, rBArBG, Angle_DEF;
    qed     by -, H2, AngleTrichotomy1;
  qed     by TetraABCD, GnotABCD, ABGcol, notABG, notBGA, -, B3', ∉;
`;;

let OppositeAnglesCongImpliesParallelogram = thm `;
  let A B C D be point;
  assume Quadrilateral A B C D                          [H1];
  assume ∡ A B C ≡ ∡ C D A  ∧  ∡ D A B ≡ ∡ B C D        [H2];
  thus Parallelogram A B C D

  proof
    Quadrilateral B C D A     [QuadBCDA] by H1, QuadrilateralSymmetry;
    ¬(A = B) ∧ ¬(B = C) ∧ ¬(C = D) ∧ ¬(D = A) ∧ ¬Collinear B C D ∧ ¬Collinear D A B     [TetraABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
    ∡ B C D ≡ ∡ D A B     [H2'] by TetraABCD, ANGLE, H2, C5Symmetric;
    consider a such that
    Line a ∧ A ∈ a ∧ B ∈ a     [a_line] by TetraABCD, I1;
    consider b such that
    Line b ∧ B ∈ b ∧ C ∈ b     [b_line] by TetraABCD, I1;
    consider c such that
    Line c  ∧ C ∈ c ∧ D ∈ c     [c_line] by TetraABCD, I1;
    consider d such that
    Line d ∧ D ∈ d ∧ A ∈ d     [d_line] by TetraABCD, I1;
  qed     by H1, QuadBCDA, H2, H2', a_line, b_line, c_line, d_line, OppositeAnglesCongImpliesParallelogramHelp, Parallelogram_DEF;
`;;


let P = new_axiom
  `∀ P l. Line l ∧ P ∉ l  ⇒ ∃! m. Line m ∧ P ∈ m ∧ m ∥ l`;;

new_constant("μ",`:point_set->real`);;

let AMa = new_axiom
 `∀ α. Angle α  ⇒  &0 < μ α ∧ μ α < &180`;;

let AMb = new_axiom
 `∀ α. Right α  ⇒  μ α  = &90`;;

let AMc = new_axiom
 `∀ α β. Angle α ∧ Angle β ∧ α ≡ β  ⇒  μ α = μ β`;;

let AMd = new_axiom
 `∀ A O B P. P ∈ int_angle A O B  ⇒  μ (∡ A O B) = μ (∡ A O P) + μ (∡ P O B)`;;


let ConverseAlternateInteriorAngles = thm `;
  let A B C E be point;
  let l m t be point_set;
  assume Line l ∧ A ∈ l ∧ E ∈ l                                   [l_line];
  assume Line m ∧ B ∈ m ∧ C ∈ m                                   [m_line];
  assume Line t ∧ A ∈ t ∧ B ∈ t                                   [t_line];
  assume ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t           [Distinct];
  assume ¬(C,E same_side t)                                        [Cnsim_tE];
  assume l ∥ m                                                     [para_lm];
  thus ∡ E A B ≡ ∡ C B A

  proof
    ¬Collinear C B A     by t_line, Distinct, I1, Collinear_DEF, ∉, ANGLE;
    A ∉ m ∧ Angle (∡ C B A)     [notAm] by m_line, -, Collinear_DEF, ∉, ANGLE;
    consider D such that
    ¬(A = D) ∧ D ∉ t ∧ ¬(C,D same_side t) ∧ seg A D ≡ seg A E  ∧  ∡ B A D ≡ ∡ C B A     [Dexists] by -,  Distinct, t_line, C4OppositeSide;
    consider k such that
    Line k ∧ A ∈ k ∧ D ∈ k     [k_line] by Distinct, I1;
    k ∥ m     by -, m_line, t_line, Dexists, Distinct, AngleSymmetry, AlternateInteriorAngles;
    k = l     by m_line, notAm, l_line, k_line, -, para_lm, P;
    D,E same_side t  ∧  A ∉ open (D,E)  ∧  Collinear A E D     by t_line, Distinct, Dexists, Cnsim_tE, AtMost2Sides, SameSide_DEF, ∉, -, k_line, l_line, Collinear_DEF;
    ray A D = ray A E     by Distinct, -, IN_Ray, Dexists, IN_DELETE, RayWellDefined;
  qed     by -, Dexists, AngleSymmetry, Angle_DEF;
`;;

let HilbertTriangleSum = thm `;
  let A B C be point;
  assume ¬Collinear A B C                               [ABCncol];
  thus ∃ E F. B ∈ open (E,F)  ∧  C ∈ int_angle A B F  ∧
           ∡ E B A ≡ ∡ C A B  ∧  ∡ C B F ≡ ∡ B C A

  proof
    ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear C A B     [Distinct] by ABCncol, NonCollinearImpliesDistinct, CollinearSymmetry;
    consider l such that
    Line l ∧ A ∈ l ∧ C ∈ l     [l_line] by Distinct, I1;
    consider x such that
    Line x ∧ A ∈ x ∧ B ∈ x     [x_line] by Distinct, I1;
    consider y such that
    Line y ∧ B ∈ y ∧ C ∈ y     [y_line] by Distinct, I1;
    C ∉ x     [notCx] by x_line, ABCncol, Collinear_DEF, ∉;
    Angle (∡ C A B)     by ABCncol, CollinearSymmetry, ANGLE;
    consider E such that
    ¬(B = E) ∧ E ∉ x ∧ ¬(C,E same_side x) ∧ seg B E ≡ seg A B ∧ ∡ A B E ≡ ∡ C A B     [Eexists] by -, Distinct, x_line, notCx, C4OppositeSide;
    consider m such that
    Line m ∧ B ∈ m ∧ E ∈ m     [m_line] by -, I1, IN_DELETE;
    ∡ E B A ≡ ∡ C A B     [EBAeqCAB] by Eexists, AngleSymmetry;
    m ∥ l     [para_lm] by m_line, l_line, x_line, Eexists, Distinct, notCx, -, AlternateInteriorAngles;
    m ∩ l = ∅     [lm0] by -, PARALLEL;
    C ∉ m ∧ A ∉ m     [notACm] by -, l_line, INTER_COMM, DisjointOneNotOther;
    consider F such that
    B ∈ open (E,F)     [EBF] by Eexists, B2';
    ¬(B = F) ∧ F ∈ m     [EBF'] by -, B1', m_line, BetweenLinear;
    ¬Collinear A B F ∧ F ∉ x      [ABFncol] by m_line, -, I1, Collinear_DEF, notACm, ∉, x_line;
    ¬(E,F same_side x) ∧ ¬(E,F same_side y)     [Ensim_yF] by EBF, x_line, y_line, SameSide_DEF;
    C,F same_side x     [Csim_xF] by x_line, notCx, Eexists, ABFncol, Eexists, -, AtMost2Sides;
    m ∩ open(C,A)  =  ∅     by l_line, BetweenLinear, SUBSET, SET_RULE, lm0, SUBSET_EMPTY;
    C,A same_side m     by m_line, -, SameSide_DEF, SET_RULE;
    C ∈ int_angle A B F     [CintABF] by ABFncol, x_line, m_line, EBF', notCx, notACm, Csim_xF, -, IN_InteriorAngle;
    A ∈ int_angle C B E     by EBF, B1', -, InteriorAngleSymmetry, InteriorReflectionInterior;
    A ∉ y  ∧  A,E same_side y     [Asim_yE] by y_line, m_line, -, InteriorUse;
    E ∉ y ∧ F ∉ y     [notEFy] by y_line, m_line, EBF', Eexists, EBF', I1, Collinear_DEF, notACm, ∉;
    E,A same_side y  by y_line, -, Asim_yE, SameSideSymmetric;
    ¬(A,F same_side y)     [Ansim_yF] by y_line, notEFy, Asim_yE, -, Ensim_yF, SameSideTransitive;
    ∡ F B C ≡ ∡ A C B     by m_line, EBF', l_line, y_line, EBF', Distinct, notEFy, Asim_yE, Ansim_yF, para_lm, ConverseAlternateInteriorAngles;
  qed     by EBF, CintABF, EBAeqCAB, -, AngleSymmetry;
`;;

let EuclidPropositionI_13 = thm `;
  let A O B A' be point;
  assume ¬Collinear A O B                       [H1];
  assume O ∈ open (A,A')                        [H2];
  thus μ (∡ A O B) + μ (∡ B O A') = &180

  proof
    cases;
    suppose Right (∡ A O B);
      Right (∡ B O A')  ∧  μ (∡ A O B) = &90  ∧  μ (∡ B O A') = &90     by H1, H2, -, RightImpliesSupplRight, AMb;
    qed by -, REAL_ARITH;
    suppose ¬Right (∡ A O B)     [notRightAOB];
      ¬(A = O) ∧ ¬(O = B)     [Distinct] by H1, NonCollinearImpliesDistinct;
      consider l such that
      Line l ∧ O ∈ l ∧ A ∈ l ∧ A' ∈ l     [l_line] by -, I1, H2, BetweenLinear;
      B ∉ l     [notBl] by -, Distinct, I1, Collinear_DEF, H1, ∉;
      consider F such that
      Right (∡ O A F)  ∧  Angle (∡ O A F)     [RightOAF] by Distinct, EuclidPropositionI_11, RightImpliesAngle;
      ∃! r. Ray r ∧ ∃ E. ¬(O = E) ∧ r = ray O E ∧ E ∉ l ∧ E,B same_side l ∧ ∡ A O E ≡ ∡ O A F     by -, Distinct, l_line, notBl, C4;
      consider E such that
      ¬(O = E)  ∧  E ∉ l  ∧  E,B same_side l  ∧  ∡ A O E ≡ ∡ O A F     [Eexists] by -;
      ¬Collinear A O E     [AOEncol] by l_line, Distinct, I1, Collinear_DEF, -, ∉;
      Right (∡ A O E)     [RightAOE] by -, ANGLE, RightOAF, Eexists, CongRightImpliesRight;
      Right (∡ E O A')  ∧  μ (∡ A O E) = &90  ∧  μ (∡ E O A') = &90     [RightEOA'] by AOEncol, H2, -,  RightImpliesSupplRight, AMb;
      ¬(∡ A O B ≡ ∡ A O E)     by notRightAOB, H1, ANGLE, RightAOE, CongRightImpliesRight;
      ¬(∡ A O B = ∡ A O E)     by H1, AOEncol, ANGLE, -, C5Reflexive;
      ¬(ray O B = ray O E)     by -, Angle_DEF;
      B ∉ ray O E  ∧  O ∉ open (B,E)     by Distinct, -, Eexists, RayWellDefined, IN_DELETE, ∉, l_line, B1', SameSide_DEF;
      ¬Collinear O E B     by -, Eexists, IN_Ray, ∉;
      E ∈ int_angle A O B  ∨  B ∈ int_angle A O E     by Distinct, l_line, Eexists, notBl, AngleOrdering, -, CollinearSymmetry, InteriorAngleSymmetry;
      cases by -;
      suppose E ∈ int_angle A O B     [EintAOB];
        B ∈ int_angle E O A'     by H2, -, InteriorReflectionInterior;
        μ (∡ A O B) = μ (∡ A O E) + μ (∡ E O B)  ∧
        μ (∡ E O A') = μ (∡ E O B) + μ (∡ B O A')     by EintAOB, -, AMd;
      qed     by -, RightEOA', REAL_ARITH;
      suppose B ∈ int_angle A O E     [BintAOE];
        E ∈ int_angle B O A'     by H2, -, InteriorReflectionInterior;
        μ (∡ A O E) = μ (∡ A O B) + μ (∡ B O E)  ∧
        μ (∡ B O A') = μ (∡ B O E) + μ (∡ E O A')     by BintAOE, -, AMd;
      qed     by -, RightEOA', REAL_ARITH;
    end;
  end;
`;;

let TriangleSum = thm `;
  let A B C be point;
  assume ¬Collinear A B C                               [ABCncol];
  thus μ (∡ A B C) + μ (∡ B C A) + μ (∡ C A B) = &180

  proof
    ¬Collinear C A B  ∧  ¬Collinear B C A     [CABncol] by ABCncol, CollinearSymmetry;
    consider E F such that
    B ∈ open (E,F)  ∧  C ∈ int_angle A B F  ∧  ∡ E B A ≡ ∡ C A B  ∧  ∡ C B F ≡ ∡ B C A     [EBF] by ABCncol, HilbertTriangleSum;
    ¬Collinear C B F  ∧  ¬Collinear A B F  ∧  Collinear E B F  ∧  ¬(B = E)     [CBFncol] by -, InteriorAngleSymmetry, InteriorEZHelp, IN_InteriorAngle, B1', CollinearSymmetry;
    ¬Collinear E B A     [EBAncol] by CollinearSymmetry, -, NoncollinearityExtendsToLine;
    μ (∡ A B F) = μ (∡ A B C) + μ (∡ C B F)     [μCintABF] by EBF, AMd;
    μ (∡ E B A) + μ (∡ A B F) = &180     [suppl180] by EBAncol, EBF, EuclidPropositionI_13;
    μ (∡ C A B) = μ (∡ E B A)  ∧  μ (∡ B C A) = μ (∡ C B F)     by CABncol, EBAncol, CBFncol, ANGLE, EBF, AMc;
  qed     by suppl180, μCintABF, -, REAL_ARITH;
`;;