RichterHilbertAxiomGeometry/HilbertAxiom_read.ml

   1 (* ========================================================================= *)
   2 (*            HOL Light Hilbert geometry axiomatic proofs                    *)
   3 (*                                                                           *)
   4 (*                (c) Copyright, Bill Richter 2013                           *)
   5 (*          Distributed under the same license as HOL Light                  *)
   6 (*                                                                           *)
   7 (* High school students can learn rigorous axiomatic geometry proofs, as in  *)
   8 (* http://www.math.northwestern.edu/~richter/hilbert.pdf, using Hilbert's    *)
   9 (* axioms, and code up readable formal proofs like these here. Thanks to the *)
  10 (* Mizar folks for their influential language, Freek Wiedijk for his dialect *)
  11 (* miz3 of HOL Light, John Harrison for explaining how to port Mizar code to *)
  12 (* miz3 and writing the first 100+ lines of code here, the hol-info list for *)
  13 (* explaining features of HOL, and Benjamin Kordesh for carefully reading    *)
  14 (* much of the paper and the code.  Formal proofs are given for the first 7  *)
  15 (* sections of the paper, the results cited there from Greenberg's book, and *)
  16 (* most of Euclid's book I propositions up to Proposition I.29, following    *)
  17 (* Hartshorne, whose book seems the most exciting axiomatic geometry text.   *)
  18 (* A proof assistant is an invaluable tool to help read it, as Hartshorne's  *)
  19 (* proofs are often sketchy and even have gaps.                              *)
  20 (*                                                                           *)
  21 (* M. Greenberg, Euclidean and non-Euclidean geometries, Freeman, 1974.      *)
  22 (* R. Hartshorne, Geometry, Euclid and Beyond, UTM series, Springer, 2000.   *)
  23 (* ========================================================================= *)
  24
  25 needs "RichterHilbertAxiomGeometry/readable.ml";;
  26
  27 new_type("point", 0);;
  28 NewConstant("Between", `:point->point->point->bool`);;
  29 NewConstant("Line", `:(point->bool)->bool`);;
  30 NewConstant("≡", `:(point->bool)->(point->bool)->bool`);;
  31
  32 ParseAsInfix("≅", (12, "right"));;
  33 ParseAsInfix("same_side", (12, "right"));;
  34 ParseAsInfix("≡", (12, "right"));;
  35 ParseAsInfix("<__", (12, "right"));;
  36 ParseAsInfix("<_ang", (12, "right"));;
  37 ParseAsInfix("suppl", (12, "right"));;
  38 ParseAsInfix("∉", (11, "right"));;
  39 ParseAsInfix("∥", (12, "right"));;
  40
  41 let NOTIN = NewDefinition `;
  42   ∀a l. a ∉ l ⇔ ¬(a ∈ l)`;;
  43
  44 let INTER_TENSOR = theorem `;
  45   ∀s s' t t'.  s ⊂ s' ∧ t ⊂ t'  ⇒  s ∩ t ⊂ s' ∩ t'
  46   by set`;;
  47
  48 let Interval_DEF = NewDefinition `;
  49   ∀A B. Open (A, B) = {X | Between A X B}`;;
  50
  51 let Collinear_DEF = NewDefinition `;
  52   Collinear A B C  ⇔
  53   ∃l. Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l`;;
  54
  55 let SameSide_DEF = NewDefinition `;
  56   A,B same_side l  ⇔
  57   Line l ∧ ¬ ∃X.  X ∈ l  ∧  X ∈ Open (A, B)`;;
  58
  59 let Ray_DEF = NewDefinition `;
  60   ∀A B. ray A B = {X | ¬(A = B) ∧ Collinear A B X ∧ A ∉ Open (X, B)}`;;
  61
  62 let Ordered_DEF = NewDefinition `;
  63   ordered A B C D  ⇔
  64   B ∈ Open (A, C) ∧ B ∈ Open (A, D) ∧ C ∈ Open (A, D) ∧ C ∈ Open (B, D)`;;
  65
  66 let InteriorAngle_DEF = NewDefinition `;
  67   ∀A O B.  int_angle A O B =
  68     {P | ¬Collinear A O B ∧ ∃a b.
  69                Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
  70                P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b}`;;
  71
  72 let InteriorTriangle_DEF = NewDefinition `;
  73   ∀A B C.  int_triangle A B C =
  74     {P | P ∈ int_angle A B C  ∧
  75          P ∈ int_angle B C A  ∧
  76          P ∈ int_angle C A B}`;;
  77
  78 let Tetralateral_DEF = NewDefinition `;
  79   Tetralateral A B C D  ⇔
  80   ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D) ∧
  81   ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B`;;
  82
  83 let Quadrilateral_DEF = NewDefinition `;
  84   Quadrilateral A B C D  ⇔
  85   Tetralateral A B C D ∧
  86   Open (A, B) ∩ Open (C, D) = ∅ ∧
  87   Open (B, C) ∩ Open (D, A) = ∅`;;
  88
  89 let ConvexQuad_DEF = NewDefinition `;
  90   ConvexQuadrilateral A B C D  ⇔
  91   Quadrilateral A B C D ∧
  92   A ∈ int_angle B C D ∧ B ∈ int_angle C D A ∧ C ∈ int_angle D A B ∧ D ∈ int_angle A B C`;;
  93
  94 let Segment_DEF = NewDefinition `;
  95   seg A B = {A, B} ∪ Open (A, B)`;;
  96
  97 let SEGMENT = NewDefinition `;
  98   Segment s  ⇔  ∃A B. s = seg A B ∧ ¬(A = B)`;;
  99
 100 let SegmentOrdering_DEF = NewDefinition `;
 101   s <__ t   ⇔
 102   Segment s ∧
 103   ∃C D X. t = seg C D ∧ X ∈ Open (C, D) ∧ s ≡ seg C X`;;
 104
 105 let Angle_DEF = NewDefinition `;
 106   ∡ A O B = ray O A ∪ ray O B`;;
 107
 108 let ANGLE = NewDefinition `;
 109   Angle α  ⇔  ∃A O B. α = ∡ A O B ∧ ¬Collinear A O B`;;
 110
 111 let AngleOrdering_DEF = NewDefinition `;
 112   α <_ang β  ⇔
 113   Angle α ∧
 114   ∃A O B G. ¬Collinear A O B  ∧  β = ∡ A O B ∧
 115              G ∈ int_angle A O B  ∧  α ≡ ∡ A O G`;;
 116
 117 let RAY = NewDefinition `;
 118   Ray r  ⇔  ∃O A. ¬(O = A) ∧ r = ray O A`;;
 119
 120 let TriangleCong_DEF = NewDefinition `;
 121   ∀A B C A' B' C'. (A, B, C) ≅ (A', B', C')  ⇔
 122   ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
 123   seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧ seg B C ≡ seg B' C' ∧
 124   ∡ A B C ≡ ∡ A' B' C' ∧
 125   ∡ B C A ≡ ∡ B' C' A' ∧
 126   ∡ C A B ≡ ∡ C' A' B'`;;
 127
 128 let SupplementaryAngles_DEF = NewDefinition `;
 129   ∀α β. α suppl β   ⇔
 130   ∃A O B A'. ¬Collinear A O B  ∧  O ∈ Open (A, A')  ∧  α = ∡ A O B  ∧  β = ∡ B O A'`;;
 131
 132 let RightAngle_DEF = NewDefinition `;
 133   ∀α. Right α  ⇔  ∃β. α suppl β ∧ α ≡ β`;;
 134
 135 let PlaneComplement_DEF = NewDefinition `;
 136   ∀α. complement α = {P | P ∉ α}`;;
 137
 138 let CONVEX = NewDefinition `;
 139   Convex α  ⇔  ∀A B. A ∈ α ∧ B ∈ α  ⇒ Open (A, B) ⊂ α`;;
 140
 141 let PARALLEL = NewDefinition `;
 142   ∀l k. l ∥ k   ⇔
 143   Line l ∧ Line k ∧ l ∩ k = ∅`;;
 144
 145 let Parallelogram_DEF = NewDefinition `;
 146   ∀A B C D. Parallelogram A B C D  ⇔
 147   Quadrilateral A B C D ∧ ∃a b c d.
 148   Line a ∧ A ∈ a ∧ B ∈ a ∧
 149   Line b ∧ B ∈ b ∧ C ∈ b ∧
 150   Line c  ∧ C ∈ c ∧ D ∈ d ∧
 151   Line d ∧ D ∈ d ∧ A ∈ d ∧
 152   a ∥ c  ∧  b ∥ d`;;
 153
 154 let InteriorCircle_DEF = NewDefinition `;
 155   ∀O R.  int_circle O R = {P | ¬(O = R) ∧ (P = O  ∨  seg O P <__ seg O R)}
 156 `;;
 157
 158
 159 (* ------------------------------------------------------------------------- *)
 160 (* Hilbert's geometry axioms, except the parallel axiom P, defined later.    *)
 161 (* ------------------------------------------------------------------------- *)
 162
 163 let I1 = NewAxiom
 164   `;∀A B.  ¬(A = B) ⇒ ∃! l. Line l ∧  A ∈ l ∧ B ∈ l`;;
 165
 166 let I2 = NewAxiom
 167   `;∀l. Line l  ⇒  ∃A B. A ∈ l ∧ B ∈ l ∧ ¬(A = B)`;;
 168
 169 let I3 = NewAxiom
 170   `;∃A B C. ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
 171                              ¬Collinear A B C`;;
 172
 173 let B1 = NewAxiom
 174   `;∀A B C. Between A B C ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
 175             Between C B A ∧ Collinear A B C`;;
 176
 177 let B2 = NewAxiom
 178   `;∀A B. ¬(A = B) ⇒ ∃C. Between A B C`;;
 179
 180 let B3 = NewAxiom
 181   `;∀A B C. ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
 182     ⇒ (Between A B C ∨ Between B C A ∨ Between C A B) ∧
 183         ¬(Between A B C ∧ Between B C A) ∧
 184         ¬(Between A B C ∧ Between C A B) ∧
 185         ¬(Between B C A ∧ Between C A B)`;;
 186
 187 let B4 = NewAxiom
 188   `;∀l A B C. Line l ∧ ¬Collinear A B C ∧
 189    A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
 190    (∃X. X ∈ l ∧ Between A X C) ⇒
 191    (∃Y. Y ∈ l ∧ Between A Y B) ∨ (∃Y. Y ∈ l ∧ Between B Y C)`;;
 192
 193 let C1 = NewAxiom
 194   `;∀s O Z. Segment s ∧ ¬(O = Z)  ⇒
 195    ∃! P. P ∈ ray O Z ━ {O}  ∧  seg O P ≡ s`;;
 196
 197 let C2Reflexive = NewAxiom
 198   `;Segment s  ⇒  s ≡ s`;;
 199
 200 let C2Symmetric = NewAxiom
 201   `;Segment s ∧ Segment t ∧ s ≡ t  ⇒  t ≡ s`;;
 202
 203 let C2Transitive = NewAxiom
 204   `;Segment s ∧ Segment t ∧ Segment u ∧
 205    s ≡ t ∧ t ≡ u ⇒  s ≡ u`;;
 206
 207 let C3 = NewAxiom
 208   `;∀A B C A' B' C'.  B ∈ Open (A, C) ∧ B' ∈ Open (A', C') ∧
 209   seg A B ≡ seg A' B' ∧ seg B C ≡ seg B' C'  ⇒
 210   seg A C ≡ seg A' C'`;;
 211
 212 let C4 = NewAxiom
 213  `;∀α O A l Y. Angle α ∧ ¬(O = A) ∧ Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l
 214     ⇒ ∃! r. Ray r  ∧  ∃B. ¬(O = B)  ∧  r = ray O B  ∧
 215           B ∉ l  ∧  B,Y same_side l  ∧  ∡ A O B ≡ α`;;
 216
 217 let C5Reflexive = NewAxiom
 218   `;Angle α  ⇒  α ≡ α`;;
 219
 220 let C5Symmetric = NewAxiom
 221   `;Angle α ∧ Angle β ∧ α ≡ β  ⇒  β ≡ α`;;
 222
 223 let C5Transitive = NewAxiom
 224   `;Angle α ∧ Angle β ∧ Angle γ ∧
 225    α ≡ β ∧ β ≡ γ ⇒  α ≡ γ`;;
 226
 227 let C6 = NewAxiom
 228   `;∀A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
 229    seg B A ≡ seg B' A' ∧ seg B C ≡ seg B' C' ∧ ∡ A B C ≡ ∡ A' B' C'
 230    ⇒ ∡ B C A ≡ ∡ B' C' A'`;;
 231
 232
 233 (* ----------------------------------------------------------------- *)
 234 (* Theorems.                                                         *)
 235 (* ----------------------------------------------------------------- *)
 236
 237 let IN_Interval = theorem `;
 238   ∀A B X. X ∈ Open (A, B)  ⇔  Between A X B
 239   by rewrite Interval_DEF IN_ELIM_THM`;;
 240
 241 let IN_Ray = theorem `;
 242   ∀A B X. X ∈ ray A B  ⇔  ¬(A = B) ∧ Collinear A B X ∧ A ∉ Open (X, B)
 243   by rewrite Ray_DEF IN_ELIM_THM`;;
 244
 245 let IN_InteriorAngle = theorem `;
 246   ∀A O B P. P ∈ int_angle A O B  ⇔
 247     ¬Collinear A O B ∧ ∃a b.
 248     Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
 249     P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b
 250   by rewrite InteriorAngle_DEF IN_ELIM_THM`;;
 251
 252 let IN_InteriorTriangle = theorem `;
 253   ∀A B C P. P ∈ int_triangle A B C  ⇔
 254     P ∈ int_angle A B C  ∧  P ∈ int_angle B C A  ∧  P ∈ int_angle C A B
 255   by rewrite InteriorTriangle_DEF IN_ELIM_THM`;;
 256
 257 let IN_PlaneComplement = theorem `;
 258   ∀α. ∀P. P ∈ complement α  ⇔  P ∉ α
 259   by rewrite PlaneComplement_DEF IN_ELIM_THM`;;
 260
 261 let IN_InteriorCircle = theorem `;
 262   ∀O R P. P ∈ int_circle O R  ⇔
 263     ¬(O = R) ∧ (P = O  ∨  seg O P <__ seg O R)
 264   by rewrite InteriorCircle_DEF IN_ELIM_THM`;;
 265
 266 let B1' = theorem `;
 267   ∀A B C.  B ∈ Open (A, C) ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
 268             B ∈ Open (C, A) ∧ Collinear A B C
 269   by fol IN_Interval B1`;;
 270
 271 let B2' = theorem `;
 272   ∀A B. ¬(A = B) ⇒ ∃C.  B ∈ Open (A, C)
 273   by fol IN_Interval B2`;;
 274
 275 let B3' = theorem `;
 276   ∀A B C. ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
 277     ⇒ (B ∈ Open (A, C) ∨ C ∈ Open (B, A) ∨ A ∈ Open (C, B)) ∧
 278        ¬(B ∈ Open (A, C) ∧ C ∈ Open (B, A)) ∧
 279        ¬(B ∈ Open (A, C) ∧ A ∈ Open (C, B)) ∧
 280        ¬(C ∈ Open (B, A) ∧ A ∈ Open (C, B))
 281   by fol IN_Interval B3`;;
 282
 283 let B4' = theorem `;
 284   ∀l A B C. Line l ∧ ¬Collinear A B C ∧
 285     A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
 286     (∃X. X ∈ l ∧  X ∈ Open (A, C)) ⇒
 287     (∃Y. Y ∈ l ∧  Y ∈ Open (A, B)) ∨ (∃Y. Y ∈ l ∧  Y ∈ Open (B, C))
 288   by rewrite IN_Interval B4`;;
 289
 290 let B4'' = theorem `;
 291   ∀l A B C.
 292   Line l ∧ ¬Collinear A B C ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l  ∧
 293   A,B same_side l  ∧  B,C same_side l  ⇒  A,C same_side l
 294   proof
 295     rewrite SameSide_DEF;
 296     fol B4';
 297   qed;
 298 `;;
 299
 300 let DisjointOneNotOther = theorem `;
 301   ∀l m. (∀x:A. x ∈ m  ⇒ x ∉ l)  ⇔  l ∩ m = ∅
 302   by fol ∉ IN_INTER MEMBER_NOT_EMPTY`;;
 303
 304 let EquivIntersectionHelp = theorem `;
 305   ∀e x:A. ∀l m:A->bool.
 306   (l ∩ m = {x}  ∨  m ∩ l = {x})  ∧  e ∈ m ━ {x}   ⇒  e ∉ l
 307   by fol ∉ IN_INTER IN_SING IN_DIFF`;;
 308
 309 let CollinearSymmetry = theorem `;
 310   ∀A B C. Collinear A B C  ⇒
 311     Collinear A C B ∧ Collinear B A C ∧ Collinear B C A ∧
 312     Collinear C A B ∧ Collinear C B A
 313
 314   proof
 315     intro_TAC ∀A B C, H1;
 316     consider l such that
 317     Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l     [l_line] by fol H1 Collinear_DEF;
 318     fol - Collinear_DEF;
 319   qed;
 320 `;;
 321
 322 let ExistsNewPointOnLine = theorem `;
 323   ∀P. Line l ∧ P ∈ l  ⇒  ∃Q. Q ∈ l ∧ ¬(P = Q)
 324
 325   proof
 326     intro_TAC ∀P, H1;
 327     consider A B such that
 328     A ∈ l ∧ B ∈ l ∧ ¬(A = B)     [l_line] by fol H1 I2;
 329     fol - l_line;
 330   qed;
 331 `;;
 332
 333 let ExistsPointOffLine = theorem `;
 334   ∀l. Line l  ⇒  ∃Q. Q ∉ l
 335
 336   proof
 337     intro_TAC ∀l, H1;
 338     consider A B C such that
 339     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear A B C     [Distinct] by fol I3;
 340     assume (A ∈ l) ∧ (B ∈ l) ∧ (C ∈ l)     [all_on] by fol ∉;
 341     Collinear A B C     [] by fol H1 - Collinear_DEF;
 342     fol - Distinct;
 343   qed;
 344 `;;
 345
 346 let BetweenLinear = theorem `;
 347   ∀A B C m. Line m ∧ A ∈ m ∧ C ∈ m  ∧
 348     (B ∈ Open (A, C) ∨ C ∈ Open (B, A)  ∨ A ∈ Open (C, B))  ⇒  B ∈ m
 349
 350   proof
 351     intro_TAC ∀A B C m, H1m H1A H1C H2;
 352     ¬(A = C) ∧
 353     (Collinear A B C ∨ Collinear B C A ∨ Collinear C A B)     [X1] by fol H2 B1';
 354     consider l such that
 355     Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l     [X2] by fol - Collinear_DEF;
 356     l = m     [] by fol X1 - H2 H1m H1A H1C I1;
 357     fol - X2;
 358   qed;
 359 `;;
 360
 361 let CollinearLinear = theorem `;
 362   ∀A B C m. Line m ∧ A ∈ m ∧ C ∈ m  ∧
 363     (Collinear A B C ∨ Collinear B C A ∨ Collinear C A B)  ∧
 364     ¬(A = C)  ⇒  B ∈ m
 365
 366   proof
 367     intro_TAC ∀A B C m, H1m H1A H1C H2 H3;
 368     consider l such that
 369     Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l     [X1] by fol H2 Collinear_DEF;
 370     l = m     [] by fol H3 - H1m H1A H1C I1;
 371     fol - X1;
 372   qed;
 373 `;;
 374
 375 let NonCollinearImpliesDistinct = theorem `;
 376   ∀A B C. ¬Collinear A B C  ⇒  ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)
 377
 378   proof
 379     intro_TAC ∀A B C, H1;
 380     assume A = B ∧ B = C     [equal] by fol H1 I1 Collinear_DEF;
 381     consider Q such that
 382     ¬(Q = A)     [notQA] by fol I3;
 383     fol - equal H1 I1 Collinear_DEF;
 384   qed;
 385 `;;
 386
 387 let NonCollinearRaa = theorem `;
 388   ∀A B C l.  ¬(A = C)  ⇒  Line l ∧ A ∈ l ∧ C ∈ l  ⇒  B ∉ l
 389     ⇒  ¬Collinear A B C
 390
 391   proof
 392     intro_TAC ∀A B C l, Distinct, l_line, notBl;
 393     assume Collinear A B C     [ANCcol] by fol;
 394     consider m such that Line m ∧ A ∈ m ∧ B ∈ m ∧ C ∈ m     [m_line] by fol - Collinear_DEF;
 395     m = l     [] by fol - l_line Distinct I1;
 396     B ∈ l     [] by fol m_line -;
 397     fol - notBl ∉;
 398   qed;
 399 `;;
 400
 401 let TwoSidesTriangle1Intersection = theorem `;
 402   ∀A B C Y. ¬Collinear A B C  ∧  Collinear B C Y  ∧  Collinear A C Y
 403      ⇒ Y = C
 404
 405   proof
 406     intro_TAC ∀A B C Y, ABCcol BCYcol ACYcol;
 407     assume ¬(C = Y)     [notCY] by fol;
 408     consider l such that
 409     Line l ∧ C ∈ l ∧ Y ∈ l     [l_line] by fol - I1;
 410     B ∈ l ∧ A ∈ l     [] by fol - BCYcol ACYcol Collinear_DEF notCY I1;
 411     fol - l_line Collinear_DEF ABCcol;
 412   qed;
 413 `;;
 414
 415 let OriginInRay = theorem `;
 416   ∀O Q. ¬(Q = O)  ⇒  O ∈ ray O Q
 417
 418   proof
 419     intro_TAC ∀O Q, H1;
 420     O ∉ Open (O, Q)     [OOQ] by fol B1' ∉;
 421     Collinear O Q O     [] by fol H1 I1 Collinear_DEF;
 422     fol H1 - OOQ IN_Ray;
 423   qed;
 424 `;;
 425
 426 let EndpointInRay = theorem `;
 427   ∀O Q. ¬(Q = O)  ⇒  Q ∈ ray O Q
 428
 429   proof
 430     intro_TAC ∀O Q, H1;
 431     O ∉ Open (Q, Q)     [notOQQ] by fol B1' ∉;
 432     Collinear O Q Q     [] by fol H1 I1 Collinear_DEF;
 433     fol H1 - notOQQ IN_Ray;
 434   qed;
 435 `;;
 436
 437 let I1Uniqueness = theorem `;
 438   ∀X l m. Line l  ∧  Line m  ∧  ¬(l = m)  ∧  X ∈ l  ∧  X ∈ m
 439      ⇒ l ∩ m = {X}
 440
 441   proof
 442     intro_TAC ∀X l m, H0l H0m H1 H2l H2m;
 443     assume ¬(l ∩ m = {X})     [H3] by fol;
 444     consider A such that
 445     A ∈ l ∩ m  ∧ ¬(A = X)     [X1] by fol H2l H2m IN_INTER H3 EXTENSION IN_SING;
 446     fol H0l H0m H2l H2m IN_INTER X1 I1 H1;
 447   qed;
 448 `;;
 449
 450 let DisjointLinesImplySameSide = theorem `;
 451   ∀l m A B.  Line l ∧ Line m ∧ A ∈ m ∧ B ∈ m ∧ l ∩ m = ∅  ⇒  A,B same_side l
 452
 453   proof
 454     intro_TAC ∀l m A B, l_line m_line Am Bm lm0;
 455       l ∩ Open (A,B) = ∅     [] by fol Am Bm m_line BetweenLinear SUBSET lm0 SUBSET_REFL INTER_TENSOR SUBSET_EMPTY;
 456       fol l_line - SameSide_DEF SUBSET IN_INTER MEMBER_NOT_EMPTY;
 457   qed;
 458 `;;
 459
 460 let EquivIntersection = theorem `;
 461   ∀A B X l m.  Line l ∧ Line m ∧ l ∩ m = {X} ∧ A ∈ m ━ {X} ∧ B ∈ m ━ {X} ∧
 462     X ∉ Open (A, B)  ⇒  A,B same_side l
 463
 464   proof
 465     intro_TAC ∀A B X l m, l_line m_line H1 H2l H2m H3;
 466     Open (A, B) ⊂ m     [] by fol l_line m_line SUBSET_DIFF IN_DIFF IN_SING  H2l H2m BetweenLinear SUBSET;
 467     l ∩ Open (A, B) ⊂ {X}     [] by fol - H1 SUBSET_REFL INTER_TENSOR;
 468     l ∩ Open (A, B) ⊂ ∅     [] by fol - SUBSET IN_SING IN_INTER H3 ∉;
 469     fol l_line - SameSide_DEF SUBSET IN_INTER NOT_IN_EMPTY;
 470   qed;
 471 `;;
 472
 473 let RayLine = theorem `;
 474   ∀O P l. Line l ∧ O ∈ l ∧ P ∈ l  ⇒  ray O P  ⊂ l
 475   by fol IN_Ray CollinearLinear SUBSET`;;
 476
 477 let RaySameSide = theorem `;
 478   ∀l O A P. Line l ∧ O ∈ l ∧ A ∉ l ∧ P ∈ ray O A ━ {O}
 479      ⇒  P ∉ l  ∧  P,A same_side l
 480
 481   proof
 482     intro_TAC ∀l O A P, l_line Ol notAl PrOA;
 483     ¬(O = A)     [notOA] by fol l_line Ol notAl ∉;
 484     consider d such that
 485     Line d ∧ O ∈ d ∧ A ∈ d     [d_line] by fol notOA I1;
 486     ¬(l = d)     [] by fol - notAl ∉;
 487     l ∩ d = {O}     [ldO] by fol l_line Ol d_line - I1Uniqueness;
 488     A ∈ d ━ {O}     [Ad_O] by fol d_line notOA IN_DIFF IN_SING;
 489     ray O A ⊂ d     [] by fol d_line RayLine;
 490     P ∈ d ━ {O}     [Pd_O] by fol PrOA - SUBSET IN_DIFF IN_SING;
 491     P ∉ l     [notPl] by fol ldO - EquivIntersectionHelp;
 492     O ∉ Open (P, A)     [] by fol PrOA IN_DIFF IN_SING IN_Ray;
 493     P,A same_side l     [] by fol l_line Ol d_line ldO Ad_O Pd_O - EquivIntersection;
 494     fol notPl -;
 495   qed;
 496 `;;
 497
 498 let IntervalRayEZ = theorem `;
 499   ∀A B C. B ∈ Open (A, C)  ⇒  B ∈ ray A C ━ {A}  ∧  C ∈ ray A B ━ {A}
 500
 501   proof
 502     intro_TAC ∀A B C, H1;
 503     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C     [ABC] by fol H1 B1';
 504     A ∉ Open (B, C)  ∧  A ∉ Open (C, B)     [] by fol - H1 B3' B1' ∉;
 505     fol ABC - CollinearSymmetry IN_Ray ∉ IN_DIFF IN_SING;
 506   qed;
 507 `;;
 508
 509 let NoncollinearityExtendsToLine = theorem `;
 510   ∀A O B X. ¬Collinear A O B  ⇒  Collinear O B X  ∧ ¬(X = O)
 511       ⇒  ¬Collinear A O X
 512
 513   proof
 514     intro_TAC ∀A O B X, H1, H2;
 515     ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
 516     consider b such that
 517     Line b ∧ O ∈ b ∧ B ∈ b     [b_line] by fol Distinct I1;
 518     A ∉ b     [notAb] by fol b_line H1 Collinear_DEF ∉;
 519     X ∈ b     [] by fol H2 b_line Distinct I1 Collinear_DEF;
 520     fol b_line - H2 notAb I1 Collinear_DEF ∉;
 521   qed;
 522 `;;
 523
 524 let SameSideReflexive = theorem `;
 525   ∀l A. Line l ∧  A ∉ l ⇒ A,A same_side l
 526   by fol B1' SameSide_DEF`;;
 527
 528 let SameSideSymmetric = theorem `;
 529   ∀l A B. Line l ∧  A ∉ l ∧ B ∉ l ⇒
 530   A,B same_side l ⇒ B,A same_side l
 531   by fol SameSide_DEF B1'`;;
 532
 533 let SameSideTransitive = theorem `;
 534   ∀l A B C. Line l  ⇒  A ∉ l ∧ B ∉ l ∧ C ∉ l  ⇒  A,B same_side l
 535     ⇒  B,C same_side l  ⇒  A,C same_side l
 536
 537   proof
 538     intro_TAC ∀l A B C, l_line, notABCl, Asim_lB, Bsim_lC;
 539     assume Collinear A B C  ∧ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [Distinct] by fol l_line notABCl Asim_lB Bsim_lC B4'' SameSideReflexive;
 540     consider m such that
 541     Line m ∧ A ∈ m ∧ C ∈ m     [m_line] by fol Distinct I1;
 542     B ∈ m     [Bm] by fol - Distinct CollinearLinear;
 543     assume ¬(m ∩ l = ∅)     [Intersect] by fol m_line l_line BetweenLinear SameSide_DEF IN_INTER NOT_IN_EMPTY;
 544     consider X such that
 545     X ∈ l ∧ X ∈ m     [Xlm] by fol - MEMBER_NOT_EMPTY IN_INTER;
 546     Collinear A X B  ∧  Collinear B A C  ∧  Collinear A B C     [ABXcol] by fol m_line Bm - Collinear_DEF;
 547     consider E such that
 548     E ∈ l ∧ ¬(E = X)     [El_X] by fol l_line Xlm ExistsNewPointOnLine;
 549     ¬Collinear E A X     [EAXncol] by fol l_line El_X Xlm notABCl I1 Collinear_DEF ∉;
 550     consider B' such that
 551     ¬(B = E)  ∧  B ∈ Open (E, B')     [EBB'] by fol notABCl El_X ∉ B2';
 552     ¬(B' = E) ∧ ¬(B' = B) ∧ Collinear B E B'     [EBB'col] by fol - B1' CollinearSymmetry;
 553     ¬Collinear A B B'  ∧  ¬Collinear B' B A  ∧  ¬Collinear B' A B     [ABB'ncol] by fol EAXncol ABXcol Distinct - NoncollinearityExtendsToLine CollinearSymmetry;
 554     ¬Collinear B' B C ∧  ¬Collinear B' A C ∧  ¬Collinear A B' C     [AB'Cncol] by fol ABB'ncol ABXcol Distinct NoncollinearityExtendsToLine CollinearSymmetry;
 555     B' ∈ ray E B ━ {E}  ∧  B ∈ ray E B' ━ {E}     [] by fol EBB' IntervalRayEZ;
 556     B' ∉ l  ∧  B',B same_side l  ∧  B,B' same_side l     [notB'l] by fol l_line El_X notABCl - RaySameSide;
 557     A,B' same_side l ∧  B',C same_side l     [] by fol l_line ABB'ncol notABCl notB'l Asim_lB - AB'Cncol Bsim_lC B4'';
 558     fol l_line AB'Cncol notABCl notB'l - B4'';
 559   qed;
 560 `;;
 561
 562 let ConverseCrossbar = theorem `;
 563   ∀O A B G. ¬Collinear A O B  ∧  G ∈ Open (A, B)  ⇒  G ∈ int_angle A O B
 564
 565   proof
 566     intro_TAC ∀O A B G, H1 H2;
 567     ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
 568     consider a such that
 569     Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by fol - I1;
 570     consider b such that
 571     Line b ∧ O ∈ b ∧ B ∈ b     [b_line] by fol Distinct I1;
 572     consider l such that
 573     Line l ∧ A ∈ l ∧ B ∈ l     [l_line] by fol Distinct I1;
 574     B ∉ a  ∧  A ∉ b     [] by fol H1 a_line  b_line Collinear_DEF ∉;
 575     ¬(a = l)  ∧  ¬(b = l)     [] by fol - l_line ∉;
 576     a ∩ l = {A}  ∧  b ∩ l = {B}     [alA] by fol - a_line l_line b_line I1Uniqueness;
 577     ¬(A = G) ∧ ¬(A = B) ∧ ¬(G = B)     [AGB] by fol H2 B1';
 578     A ∉ Open (G, B)  ∧  B ∉ Open (G, A)     [notGAB] by fol H2 B3' B1' ∉;
 579     G ∈ l     [Gl] by fol l_line H2 BetweenLinear;
 580     G ∉ a  ∧  G ∉ b     [notGa] by fol alA Gl AGB IN_DIFF IN_SING EquivIntersectionHelp;
 581     G ∈ l ━ {A} ∧ B ∈ l ━ {A} ∧ G ∈ l ━ {B} ∧ A ∈ l ━ {B}      [] by fol Gl l_line AGB IN_DIFF IN_SING;
 582     G,B same_side a  ∧  G,A same_side b     [] by fol a_line l_line alA - notGAB b_line EquivIntersection;
 583     fol H1 a_line b_line notGa - IN_InteriorAngle;
 584   qed;
 585 `;;
 586
 587 let InteriorUse = theorem `;
 588   ∀A O B P a b.
 589     Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b  ⇒
 590     P  ∈ int_angle A O B  ⇒
 591     P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b
 592
 593   proof
 594     intro_TAC ∀A O B P a b, aOAbOB, P_AOB;
 595     consider α β such that ¬Collinear A O B ∧
 596     Line α ∧ O ∈ α ∧ A ∈ α ∧
 597     Line β ∧ O ∈ β ∧B ∈ β ∧
 598     P ∉ α ∧ P ∉ β ∧
 599     P,B same_side α ∧ P,A same_side β     [exists] by fol P_AOB IN_InteriorAngle;
 600     ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B)     [] by fol - NonCollinearImpliesDistinct;
 601     α = a ∧ β = b     [] by fol - aOAbOB exists I1;
 602     fol - exists;
 603   qed;
 604 `;;
 605
 606 let InteriorEZHelp = theorem `;
 607   ∀A O B P. P ∈ int_angle A O B  ⇒
 608   ¬(P = A) ∧ ¬(P = O) ∧ ¬(P = B) ∧ ¬Collinear A O P
 609
 610   proof
 611     intro_TAC ∀A O B P, P_AOB;
 612     consider a b such that
 613     ¬Collinear A O B ∧
 614     Line a ∧ O ∈ a ∧ A ∈ a ∧
 615     Line b ∧ O ∈ b ∧B ∈ b ∧
 616     P ∉ a ∧ P ∉ b     [def_int] by fol P_AOB IN_InteriorAngle;
 617     ¬(P = A) ∧ ¬(P = O) ∧ ¬(P = B)     [PnotAOB] by fol - ∉;
 618     ¬(A = O)     [] by fol def_int NonCollinearImpliesDistinct;
 619     ¬Collinear A O P     [] by fol def_int - NonCollinearRaa CollinearSymmetry;
 620     fol PnotAOB -;
 621   qed;
 622 `;;
 623
 624 let InteriorAngleSymmetry = theorem `;
 625   ∀A O B P: point. P ∈ int_angle A O B  ⇒  P ∈ int_angle B O A
 626
 627   proof     rewrite IN_InteriorAngle;     fol CollinearSymmetry;     qed;
 628 `;;
 629
 630 let InteriorWellDefined = theorem `;
 631   ∀A O B X P. P ∈ int_angle A O B  ∧  X ∈ ray O B ━ {O}  ⇒  P ∈ int_angle A O X
 632
 633   proof
 634     intro_TAC ∀A O B X P, H1 H2;
 635     consider a b such that
 636     ¬Collinear A O B ∧
 637     Line a ∧ O ∈ a ∧ A ∈ a ∧ P ∉ a     ∧     Line b ∧ O ∈ b ∧ B ∈ b ∧ P ∉ b ∧
 638     P,B same_side a ∧ P,A same_side b     [def_int] by fol H1 IN_InteriorAngle;
 639     ¬(X = O) ∧ ¬(O = B) ∧ Collinear O B X     [H2'] by fol H2 IN_Ray IN_DIFF IN_SING;
 640     B ∉ a     [notBa] by fol def_int Collinear_DEF ∉;
 641     ¬Collinear A O X     [AOXnoncol] by fol def_int H2' NoncollinearityExtendsToLine;
 642     X ∈ b     [Xb] by fol def_int H2' CollinearLinear;
 643     X ∉ a  ∧  B,X same_side a     [] by fol def_int notBa H2 RaySameSide SameSideSymmetric;
 644     P,X same_side a     [] by fol def_int - notBa SameSideTransitive;
 645     fol AOXnoncol def_int Xb - IN_InteriorAngle;
 646   qed;
 647 `;;
 648
 649 let WholeRayInterior = theorem `;
 650   ∀A O B X P. X ∈ int_angle A O B  ∧  P ∈ ray O X ━ {O}  ⇒  P ∈ int_angle A O B
 651
 652   proof
 653     intro_TAC ∀A O B X P, XintAOB PrOX;
 654     consider a b such that
 655     ¬Collinear A O B ∧
 656     Line a ∧ O ∈ a ∧ A ∈ a ∧ X ∉ a   ∧   Line b ∧ O ∈ b ∧ B ∈ b ∧ X ∉ b ∧
 657     X,B same_side a ∧ X,A same_side b     [def_int] by fol XintAOB IN_InteriorAngle;
 658     P ∉ a ∧ P,X same_side a ∧ P ∉ b ∧ P,X same_side b     [Psim_abX] by fol def_int PrOX RaySameSide;
 659     P,B same_side a  ∧ P,A same_side b     [] by fol - def_int Collinear_DEF SameSideTransitive ∉;
 660        fol def_int Psim_abX - IN_InteriorAngle;
 661   qed;
 662 `;;
 663
 664 let AngleOrdering = theorem `;
 665   ∀O A P Q a. ¬(O = A)  ⇒  Line a ∧ O ∈ a ∧ A ∈ a  ⇒
 666     P ∉ a ∧ Q ∉ a  ⇒  P,Q same_side a  ⇒  ¬Collinear P O Q  ⇒
 667     P ∈ int_angle Q O A  ∨  Q ∈ int_angle P O A
 668
 669   proof
 670     intro_TAC ∀O A P Q a, H1, H2, H3, H4, H5;
 671     ¬(P = O) ∧ ¬(P = Q) ∧ ¬(O = Q)     [Distinct] by fol H5 NonCollinearImpliesDistinct;
 672     consider q such that
 673     Line q ∧ O ∈ q ∧ Q ∈ q     [q_line] by fol Distinct I1;
 674     P ∉ q     [notPq] by fol - H5 Collinear_DEF ∉;
 675     assume ¬(P ∈ int_angle Q O A)     [notPintQOA] by fol;
 676     ¬Collinear Q O A  ∧  ¬Collinear P O A     [POAncol] by fol H1 H2 H3 I1 Collinear_DEF ∉;
 677 ¬(P,A same_side q)     [] by fol - H2 q_line H3 notPq H4 notPintQOA IN_InteriorAngle;
 678     consider G such that
 679     G ∈ q ∧ G ∈ Open (P, A)     [existG] by fol q_line - SameSide_DEF;
 680     G ∈ int_angle P O A     [G_POA] by fol POAncol existG ConverseCrossbar;
 681     G ∉ a ∧ G,P same_side a ∧ ¬(G = O)     [Gsim_aP] by fol - H1 H2 IN_InteriorAngle I1 ∉;
 682     G,Q same_side a     [] by fol H2 Gsim_aP H3 H4 SameSideTransitive;
 683     O ∉ Open (Q, G)     [notQOG] by fol - H2 SameSide_DEF B1' ∉;
 684     Collinear O G Q     [] by fol q_line existG Collinear_DEF;
 685     Q ∈ ray O G ━ {O}     [] by fol Gsim_aP - notQOG Distinct IN_Ray IN_DIFF IN_SING;
 686     fol G_POA - WholeRayInterior;
 687   qed;
 688 `;;
 689
 690 let InteriorsDisjointSupplement = theorem `;
 691   ∀A O B A'. ¬Collinear A O B  ∧  O ∈ Open (A, A')  ⇒
 692     int_angle B O A'  ∩  int_angle A O B = ∅
 693
 694   proof
 695     intro_TAC ∀A O B A', H1 H2;
 696     ∀D. D ∈ int_angle A O B  ⇒  D ∉ int_angle B O A'     []
 697     proof
 698       intro_TAC ∀D, H3;
 699       ¬(A = O) ∧ ¬(O = B)     [] by fol H1 NonCollinearImpliesDistinct;
 700       consider a b such that
 701       Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧ A' ∈ a     [ab_line] by fol - H2 I1 BetweenLinear;
 702       ¬Collinear B O A'     [] by fol H1 H2 CollinearSymmetry B1' NoncollinearityExtendsToLine;
 703       A ∉ b  ∧  A' ∉ b     [notAb] by fol ab_line H1 - Collinear_DEF ∉;
 704       ¬(A',A same_side b)     [A'nsim_bA] by fol ab_line H2 B1' SameSide_DEF;
 705       D ∉ b  ∧  D,A same_side b     [DintAOB] by fol ab_line H3 InteriorUse;
 706       ¬(D,A' same_side b)     [] by fol ab_line notAb DintAOB A'nsim_bA SameSideSymmetric SameSideTransitive;
 707       fol ab_line - InteriorUse ∉;
 708     qed;
 709     fol - DisjointOneNotOther;
 710   qed;
 711 `;;
 712
 713 let InteriorReflectionInterior = theorem `;
 714   ∀A O B D A'. O ∈ Open (A, A')  ∧  D ∈ int_angle A O B  ⇒
 715     B  ∈ int_angle D O A'
 716
 717   proof
 718     intro_TAC ∀A O B D A', H1 H2;
 719     consider a b such that
 720     ¬Collinear A O B ∧ Line a ∧ O ∈ a ∧ A ∈ a ∧ D ∉ a ∧
 721     Line b ∧ O ∈ b ∧ B ∈ b ∧ D ∉ b ∧ D,B same_side a     [DintAOB] by fol H2 IN_InteriorAngle;
 722     ¬(O = B) ∧ ¬(O = A') ∧ B ∉ a     [Distinct] by fol - H1 NonCollinearImpliesDistinct B1' Collinear_DEF ∉;
 723     ¬Collinear D O B     [DOB_ncol] by fol DintAOB - NonCollinearRaa CollinearSymmetry;
 724     A' ∈ a     [A'a] by fol H1 DintAOB BetweenLinear;
 725     D ∉ int_angle B O A'     [] by fol DintAOB H1 H2 InteriorsDisjointSupplement DisjointOneNotOther;
 726     fol Distinct DintAOB A'a DOB_ncol - AngleOrdering ∉;
 727   qed;
 728 `;;
 729
 730 let Crossbar_THM = theorem `;
 731   ∀O A B D. D ∈ int_angle A O B  ⇒  ∃G. G ∈ Open (A, B)  ∧  G ∈ ray O D ━ {O}
 732
 733   proof
 734     intro_TAC ∀O A B D, H1;
 735     consider a b such that
 736     ¬Collinear A O B ∧
 737     Line a ∧ O ∈ a ∧ A ∈ a ∧
 738     Line b ∧ O ∈ b ∧ B ∈ b ∧
 739     D ∉ a ∧ D ∉ b ∧ D,B same_side a ∧ D,A same_side b     [DintAOB] by fol H1 IN_InteriorAngle;
 740     B ∉ a     [notBa] by fol DintAOB Collinear_DEF ∉;
 741     ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B) ∧ ¬(D = O)     [Distinct] by fol DintAOB NonCollinearImpliesDistinct ∉;
 742     consider l such that
 743     Line l ∧ O ∈ l ∧ D ∈ l     [l_line] by fol - I1;
 744     consider A' such that
 745     O ∈ Open (A, A')     [AOA'] by fol Distinct B2';
 746     A' ∈ a ∧ Collinear A O A' ∧ ¬(A' = O)      [A'a] by fol DintAOB - BetweenLinear B1';
 747     ¬(A,A' same_side l)     [Ansim_lA'] by fol l_line AOA' SameSide_DEF;
 748     B ∈ int_angle D O A'     [] by fol H1 AOA' InteriorReflectionInterior;
 749     B,A' same_side l     [Bsim_lA'] by fol l_line DintAOB A'a - InteriorUse;
 750     ¬Collinear A O D  ∧  ¬Collinear B O D      [AODncol] by fol H1 InteriorEZHelp InteriorAngleSymmetry;
 751     ¬Collinear D O A'      [] by fol - A'a CollinearSymmetry NoncollinearityExtendsToLine;
 752     A ∉ l ∧ B ∉ l ∧ A' ∉ l     [] by fol l_line AODncol - Collinear_DEF ∉;
 753     ¬(A,B same_side l)     [] by fol l_line - Bsim_lA' Ansim_lA' SameSideTransitive;
 754     consider G such that
 755     G ∈ Open (A, B) ∧ G ∈ l     [AGB] by fol l_line - SameSide_DEF;
 756     Collinear O D G     [ODGcol] by fol - l_line Collinear_DEF;
 757     G ∈ int_angle A O B     [] by fol DintAOB AGB ConverseCrossbar;
 758     G ∉ a  ∧  G,B same_side a  ∧  ¬(G = O)     [Gsim_aB] by fol DintAOB - InteriorUse ∉;
 759     B,D same_side a     [] by fol DintAOB notBa SameSideSymmetric;
 760     G,D same_side a     [Gsim_aD] by fol DintAOB Gsim_aB notBa - SameSideTransitive;
 761     O ∉ Open (G, D)     [] by fol DintAOB - SameSide_DEF ∉;
 762     G ∈ ray O D ━ {O}     [] by fol Distinct ODGcol - Gsim_aB IN_Ray IN_DIFF IN_SING;
 763     fol AGB -;
 764   qed;
 765 `;;
 766
 767 let AlternateConverseCrossbar = theorem `;
 768   ∀O A B G. Collinear A G B  ∧  G ∈ int_angle A O B  ⇒  G ∈ Open (A, B)
 769
 770   proof
 771     intro_TAC ∀O A B G, H1;
 772     consider a b such that
 773     ¬Collinear A O B  ∧  Line a ∧ O ∈ a ∧ A ∈ a  ∧  Line b ∧ O ∈ b ∧ B ∈ b  ∧
 774     G,B same_side a  ∧  G,A same_side b     [GintAOB] by fol H1 IN_InteriorAngle;
 775     ¬(A = B) ∧ ¬(G = A) ∧ ¬(G = B)  ∧  A ∉ Open (G, B)  ∧  B ∉ Open (G, A)     [] by fol - H1 NonCollinearImpliesDistinct InteriorEZHelp SameSide_DEF ∉;
 776     fol - H1 B1' B3' ∉;
 777   qed;
 778 `;;
 779
 780 let InteriorOpposite = theorem `;
 781   ∀A O B P p. P ∈ int_angle A O B  ⇒  Line p ∧ O ∈ p ∧ P ∈ p
 782     ⇒  ¬(A,B same_side p)
 783
 784   proof
 785     intro_TAC ∀A O B P p, PintAOB, p_line;
 786     consider G such that
 787     G ∈ Open (A, B) ∧ G ∈ ray O P     [Gexists] by fol PintAOB Crossbar_THM IN_DIFF;
 788     fol p_line p_line - RayLine SUBSET Gexists SameSide_DEF;
 789   qed;
 790 `;;
 791
 792 let IntervalTransitivity = theorem `;
 793   ∀O P Q R m. Line m  ∧ O ∈ m  ⇒  P ∈ m ━ {O} ∧ Q ∈ m ━ {O} ∧ R ∈ m ━ {O}  ⇒
 794     O ∉ Open (P, Q) ∧ O ∉ Open (Q, R)  ⇒  O ∉ Open (P, R)
 795
 796   proof
 797     intro_TAC ∀O P Q R m, H0, H2, H3;
 798     consider E such that
 799     E ∉ m ∧  ¬(O = E)     [notEm] by fol H0 ExistsPointOffLine ∉;
 800     consider l such that
 801     Line l ∧ O ∈ l ∧ E ∈ l     [l_line] by fol - I1;
 802     ¬(m = l)     [] by fol notEm - ∉;
 803     l ∩ m = {O}     [lmO] by fol l_line H0 - l_line I1Uniqueness;
 804     P ∉ l ∧  Q ∉ l ∧ R ∉ l     [notPQRl] by fol - H2 EquivIntersectionHelp;
 805     P,Q same_side l  ∧  Q,R same_side l     [] by fol l_line H0 lmO H2 H3 EquivIntersection;
 806     P,R same_side l     [Psim_lR] by fol l_line notPQRl - SameSideTransitive;
 807     fol l_line - SameSide_DEF ∉;
 808   qed;
 809 `;;
 810
 811 let RayWellDefinedHalfway = theorem `;
 812   ∀O P Q. ¬(Q = O)  ∧  P ∈ ray O Q ━ {O}  ⇒  ray O P ⊂ ray O Q
 813
 814   proof
 815     intro_TAC ∀O P Q, H1 H2;
 816     consider m such that
 817     Line m ∧ O ∈ m ∧ Q ∈ m     [OQm] by fol H1 I1;
 818     P ∈ ray O Q  ∧  ¬(P = O)  ∧  O ∉ Open (P, Q)     [H2'] by fol H2 IN_Ray IN_DIFF IN_SING;
 819     P ∈ m  ∧  P ∈ m ━ {O}  ∧  Q ∈ m ━ {O}     [PQm_O] by fol OQm H2' RayLine SUBSET H2' OQm H1 IN_DIFF IN_SING;
 820     O ∉ Open (P, Q)     [notPOQ] by fol H2' IN_Ray;
 821     rewrite SUBSET;
 822     X_genl_TAC X;    intro_TAC XrayOP;
 823     X ∈ m  ∧  O ∉ Open (X, P)     [XrOP] by fol - SUBSET OQm PQm_O H2' RayLine IN_Ray;
 824     Collinear O Q X     [OQXcol] by fol OQm -  Collinear_DEF;
 825     assume ¬(X = O)     [notXO] by fol H1 OriginInRay;
 826     X ∈ m ━ {O}     [] by fol XrOP - IN_DIFF IN_SING;
 827     O ∉ Open (X, Q)     [] by fol OQm - PQm_O XrOP H2' IntervalTransitivity;
 828     fol H1 OQXcol - IN_Ray;
 829   qed;
 830 `;;
 831
 832 let RayWellDefined = theorem `;
 833   ∀O P Q. ¬(Q = O)  ∧  P ∈ ray O Q ━ {O}  ⇒  ray O P = ray O Q
 834
 835   proof
 836     intro_TAC ∀O P Q, H1  H2;
 837     ray O P ⊂ ray O Q     [PsubsetQ] by fol H1 H2 RayWellDefinedHalfway;
 838     ¬(P = O)  ∧  Collinear O Q P  ∧  O ∉ Open (P, Q)     [H2'] by fol H2 IN_Ray IN_DIFF IN_SING;
 839     Q ∈ ray O P ━ {O}     [] by fol H2' B1' ∉ CollinearSymmetry IN_Ray H1 IN_DIFF IN_SING;
 840     ray O Q ⊂ ray O P     [QsubsetP] by fol H2' - RayWellDefinedHalfway;
 841     fol PsubsetQ QsubsetP SUBSET_ANTISYM;
 842   qed;
 843 `;;
 844
 845 let OppositeRaysIntersect1pointHelp = theorem `;
 846   ∀A O B X. O ∈ Open (A, B)  ∧  X ∈ ray O B ━ {O}
 847     ⇒  X ∉ ray O A  ∧  O ∈ Open (X, A)
 848
 849   proof
 850     intro_TAC ∀A O B X, H1 H2;
 851     ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B) ∧ Collinear A O B     [AOB] by fol H1 B1';
 852     ¬(X = O) ∧ Collinear O B X ∧ O ∉ Open (X, B)     [H2'] by fol H2 IN_Ray IN_DIFF IN_SING;
 853     consider m such that
 854     Line m ∧ A ∈ m ∧ B ∈ m     [m_line] by fol AOB I1;
 855     O ∈ m  ∧ X ∈ m     [Om] by fol m_line H2' AOB CollinearLinear;
 856     A ∈ m ━ {O}  ∧  X ∈ m ━ {O}  ∧  B ∈ m ━ {O}     [] by fol m_line - H2' AOB IN_DIFF IN_SING;
 857     fol H1 m_line Om - H2' IntervalTransitivity ∉ B1' IN_Ray;
 858   qed;
 859 `;;
 860
 861 let OppositeRaysIntersect1point = theorem `;
 862   ∀A O B. O ∈ Open (A, B)  ⇒  ray O A ∩ ray O B  =  {O}
 863
 864   proof
 865     intro_TAC ∀A O B, H1;
 866     ¬(A = O) ∧ ¬(O = B)     [] by fol H1 B1';
 867     rewrite GSYM SUBSET_ANTISYM_EQ SUBSET IN_INTER;
 868     conj_tac     [Right] by fol - OriginInRay IN_SING;
 869     fol H1 OppositeRaysIntersect1pointHelp IN_DIFF IN_SING ∉;
 870   qed;
 871 `;;
 872
 873 let IntervalRay = theorem `;
 874   ∀A B C. B ∈ Open (A, C)  ⇒  ray A B = ray A C
 875   by fol B1' IntervalRayEZ RayWellDefined`;;
 876
 877 let Reverse4Order = theorem `;
 878   ∀A B C D. ordered A B C D  ⇒  ordered D C B A
 879   proof
 880     rewrite Ordered_DEF;
 881     fol B1';
 882   qed;
 883 `;;
 884
 885 let TransitivityBetweennessHelp = theorem `;
 886   ∀A B C D. B ∈ Open (A, C)  ∧  C ∈ Open (B, D)
 887    ⇒  B ∈ Open (A, D)
 888
 889   proof
 890     intro_TAC ∀A B C D, H1;
 891     D ∈ ray B C ━ {B}     [] by fol H1 IntervalRayEZ;
 892     fol H1 - OppositeRaysIntersect1pointHelp B1';
 893   qed;
 894 `;;
 895
 896 let TransitivityBetweenness = theorem `;
 897   ∀A B C D. B ∈ Open (A, C)  ∧  C ∈ Open (B, D)  ⇒  ordered A B C D
 898
 899   proof
 900     intro_TAC ∀A B C D, H1;
 901     B ∈ Open (A, D)     [ABD] by fol H1 TransitivityBetweennessHelp;
 902     C ∈ Open (D, B)  ∧  B ∈ Open (C, A)     [] by fol H1 B1';
 903     C ∈ Open (D, A)     [] by fol - TransitivityBetweennessHelp;
 904     fol H1 ABD - B1' Ordered_DEF;
 905   qed;
 906 `;;
 907
 908 let IntervalsAreConvex = theorem `;
 909   ∀A B C. B ∈ Open (A, C)  ⇒  Open (A, B)  ⊂  Open (A, C)
 910
 911   proof
 912     intro_TAC ∀A B C, H1;
 913     ∀X. X ∈ Open (A, B)  ⇒  X ∈ Open (A, C)     []
 914     proof
 915       intro_TAC ∀X, AXB;
 916       X ∈ ray B A ━ {B}     [] by fol AXB B1' IntervalRayEZ;
 917       B ∈ Open (X, C)     [] by fol H1 B1' - OppositeRaysIntersect1pointHelp;
 918       fol AXB - TransitivityBetweennessHelp;
 919     qed;
 920     fol - SUBSET;
 921   qed;
 922 `;;
 923
 924 let TransitivityBetweennessVariant = theorem `;
 925   ∀A X B C. X ∈ Open (A, B)  ∧  B ∈ Open (A, C)  ⇒  ordered A X B C
 926
 927   proof
 928     intro_TAC ∀A X B C, H1;
 929     X ∈ ray B A ━ {B}     [] by fol H1 B1' IntervalRayEZ;
 930     B ∈ Open (X, C)     [] by fol H1 B1' - OppositeRaysIntersect1pointHelp;
 931     fol H1 - TransitivityBetweenness;
 932   qed;
 933 `;;
 934
 935 let Interval2sides2aLineHelp = theorem `;
 936   ∀A B C X. B ∈ Open (A, C)  ⇒  X ∉ Open (A, B) ∨ X ∉ Open (B, C)
 937
 938   proof
 939     intro_TAC ∀A B C X, H1;
 940     assume ¬(X ∉ Open (A, B))     [AXB] by fol;
 941     ordered A X B C     [] by fol - ∉ H1 TransitivityBetweennessVariant;
 942     fol MESON [-; Ordered_DEF] [B ∈ Open (X, C)] B1' B3' ∉;
 943   qed;
 944 `;;
 945
 946 let Interval2sides2aLine = theorem `;
 947   ∀A B C X. Collinear A B C
 948     ⇒  X ∉ Open (A, B)  ∨  X ∉ Open (A, C)  ∨  X ∉ Open (B, C)
 949
 950   proof
 951     intro_TAC ∀A B C X, H1;
 952     assume ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [Distinct] by fol B1' ∉;
 953     B ∈ Open (A, C)  ∨  C ∈ Open (B, A)  ∨  A ∈ Open (C, B)     [] by fol - H1 B3';
 954     fol - Interval2sides2aLineHelp B1' ∉;
 955   qed;
 956 `;;
 957
 958 let TwosidesTriangle2aLine = theorem `;
 959   ∀A B C l. Line l ∧ ¬Collinear A B C  ⇒  A ∉ l ∧ B ∉ l ∧ C ∉ l  ⇒
 960     ¬(A,B same_side l) ∧ ¬(B,C same_side l)  ⇒  A,C same_side l
 961
 962   proof
 963     intro_TAC ∀ A B C l, H1, off_l, H2;
 964     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [ABCdistinct] by fol H1 NonCollinearImpliesDistinct;
 965     consider m such that
 966     Line m ∧ A ∈ m ∧ C ∈ m     [m_line] by fol - I1;
 967     assume ¬(l ∩ m = ∅)     [lmIntersect] by fol H1 m_line DisjointLinesImplySameSide;
 968     consider Y such that
 969     Y ∈ l ∧ Y ∈ m     [Ylm] by fol lmIntersect MEMBER_NOT_EMPTY IN_INTER;
 970     consider X Z such that
 971     X ∈ l  ∧  X ∈ Open (A, B)  ∧  Z ∈ l  ∧  Z ∈ Open (C, B)     [H2'] by fol H1 H2 SameSide_DEF B1';
 972     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Y ∈ m ━ {A}  ∧  Y ∈ m ━ {C}  ∧  C ∈ m ━ {A}  ∧  A ∈ m ━ {C}     [Distinct] by fol H1 NonCollinearImpliesDistinct Ylm off_l ∉ m_line IN_DIFF IN_SING;
 973     consider p such that
 974     Line p ∧ B ∈ p ∧ A ∈ p     [p_line] by fol Distinct I1;
 975     consider q such that
 976     Line q ∧ B ∈ q ∧ C ∈ q     [q_line] by fol Distinct I1;
 977     X ∈ p  ∧ Z ∈ q     [Xp] by fol p_line H2' BetweenLinear q_line H2';
 978     A ∉ q ∧ B ∉ m ∧ C ∉ p     [vertex_off_line] by fol q_line m_line p_line H1 Collinear_DEF ∉;
 979     X ∉ q  ∧  X,A same_side q  ∧  Z ∉ p  ∧  Z,C same_side p     [Xsim_qA] by fol q_line p_line - H2' B1' IntervalRayEZ RaySameSide;
 980     ¬(m = p)  ∧  ¬(m = q)     [] by fol m_line vertex_off_line ∉;
 981     p ∩ m = {A}  ∧  q ∩ m = {C}     [pmA] by fol p_line m_line q_line H1 - Xp H2' I1Uniqueness;
 982     Y ∉ p  ∧  Y ∉ q     [notYpq] by fol - Distinct EquivIntersectionHelp;
 983     X ∈ ray A B ━ {A}  ∧  Z ∈ ray C B ━ {C}     [] by fol H2' IntervalRayEZ H2' B1';
 984     X ∉ m  ∧  Z ∉ m  ∧  X,B same_side m  ∧  B,Z same_side m     [notXZm] by fol m_line vertex_off_line - RaySameSide SameSideSymmetric;
 985     X,Z same_side m     [] by fol m_line - vertex_off_line SameSideTransitive;
 986     Collinear X Y Z ∧ Y ∉ Open (X, Z) ∧  ¬(Y = X) ∧ ¬(Y = Z) ∧ ¬(X = Z)     [] by fol H1 H2' Ylm Collinear_DEF m_line - SameSide_DEF notXZm Xsim_qA Xp ∉;
 987     Z ∈ Open (X, Y)  ∨  X ∈ Open (Z, Y)     [] by fol - B3' ∉ B1';
 988     case_split ZXY | XZY     by fol -;
 989     suppose X ∈ Open (Z, Y);
 990       ¬(Z,Y same_side p)     [] by fol p_line Xp - SameSide_DEF;
 991       ¬(C,Y same_side p)     [] by fol p_line Xsim_qA vertex_off_line notYpq - SameSideTransitive;
 992       A ∈ Open (C, Y)     [] by fol p_line m_line pmA Distinct - EquivIntersection ∉;
 993       fol H1 Ylm off_l - B1' IntervalRayEZ RaySameSide;
 994     end;
 995     suppose Z ∈ Open (X, Y);
 996       ¬(X,Y same_side q)     [] by fol q_line Xp - SameSide_DEF;
 997       ¬(A,Y same_side q)     [] by fol q_line Xsim_qA vertex_off_line notYpq - SameSideTransitive;
 998       C ∈ Open (Y, A)     [] by fol q_line m_line pmA Distinct - EquivIntersection ∉ B1';
 999       fol H1 Ylm off_l - IntervalRayEZ RaySameSide;
1000     end;
1001   qed;
1002 `;;
1003
1004 let LineUnionOf2Rays = theorem `;
1005   ∀A O B l. Line l ∧ A ∈ l ∧ B ∈ l  ⇒  O ∈ Open (A, B)
1006    ⇒  l = ray O A ∪ ray O B
1007
1008   proof
1009     intro_TAC ∀A O B l, H1, H2;
1010     ¬(A = O) ∧ ¬(O = B) ∧ O ∈ l     [Distinct] by fol H2 B1' H1 BetweenLinear;
1011     ray O A ∪ ray O B  ⊂  l     [AOBsub_l] by fol H1 - RayLine UNION_SUBSET;
1012     ∀X. X ∈ l  ⇒  X ∈ ray O A  ∨  X ∈ ray O B     []
1013     proof
1014       intro_TAC ∀X, Xl;
1015       assume ¬(X ∈ ray O B)     [notXrOB] by fol;
1016       Collinear O B X  ∧  Collinear X A B  ∧  Collinear O A X     [XABcol] by fol Distinct H1 Xl Collinear_DEF;
1017       O ∈ Open (X, B)     [] by fol notXrOB Distinct - IN_Ray ∉;
1018       O ∉ Open (X, A)     [] by fol ∉ B1' XABcol - H2 Interval2sides2aLine;
1019       fol Distinct XABcol - IN_Ray;
1020     qed;
1021     l ⊂ ray O A ∪ ray O B     [] by fol - IN_UNION SUBSET;
1022     fol - AOBsub_l SUBSET_ANTISYM;
1023   qed;
1024 `;;
1025
1026 let AtMost2Sides = theorem `;
1027   ∀A B C l.  Line l  ⇒  A ∉ l ∧ B ∉ l ∧ C ∉ l
1028    ⇒  A,B same_side l  ∨  A,C same_side l  ∨  B,C same_side l
1029
1030   proof
1031     intro_TAC ∀A B C l, l_line, H2;
1032     assume ¬(A = C)     [notAC] by fol l_line H2 SameSideReflexive;
1033     assume Collinear A B C     [ABCcol] by fol l_line H2 TwosidesTriangle2aLine;
1034     consider m such that
1035     Line m ∧ A ∈ m ∧ B ∈ m ∧ C ∈ m     [m_line] by fol notAC - I1 Collinear_DEF;
1036     assume ¬(m ∩ l = ∅)     [m_lNot0] by fol m_line l_line BetweenLinear SameSide_DEF IN_INTER NOT_IN_EMPTY;
1037     consider X such that
1038     X ∈ l ∧ X ∈ m     [Xlm] by fol - IN_INTER MEMBER_NOT_EMPTY;
1039     A ∈ m ━ {X}  ∧  B ∈ m ━ {X}  ∧  C ∈ m ━ {X}     [ABCm_X] by fol m_line - H2 ∉ IN_DIFF IN_SING;
1040     X ∉ Open (A, B)  ∨  X ∉ Open (A, C)  ∨  X ∉ Open (B, C)     [] by fol ABCcol Interval2sides2aLine;
1041     fol l_line m_line m_line Xlm H2 ∉ I1Uniqueness ABCm_X - EquivIntersection;
1042   qed;
1043 `;;
1044
1045 let FourPointsOrder = theorem `;
1046   ∀A B C X l.  Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ X ∈ l  ⇒
1047     ¬(X = A) ∧ ¬(X = B) ∧ ¬(X = C)  ⇒  B ∈ Open (A, C)
1048    ⇒  ordered X A B C  ∨  ordered A X B C  ∨
1049        ordered A B X C  ∨  ordered A B C X
1050
1051   proof
1052     intro_TAC ∀A B C X l, H1, H2, H3;
1053     A ∈ Open (X, B)  ∨  X ∈ Open (A, B)  ∨  X ∈ Open (B, C)  ∨  C ∈ Open (B, X)     []
1054     proof
1055       ¬(A = B) ∧ ¬(B = C)     [ABCdistinct] by fol H3 B1';
1056       Collinear A B X ∧ Collinear A C X ∧ Collinear C B X     [ACXcol] by fol H1 Collinear_DEF;
1057       A ∈ Open (X, B)  ∨  X ∈ Open (A, B)  ∨  B ∈ Open (A, X)     [3pos] by fol H2 ABCdistinct - B3' B1';
1058       assume B ∈ Open (A, X)     [ABX] by fol 3pos;
1059       B ∉ Open (C, X)     [] by fol ACXcol H3 - Interval2sides2aLine ∉;
1060       fol H2 ABCdistinct ACXcol - B3' B1' ∉;
1061     qed;
1062     fol - H3 B1' TransitivityBetweenness TransitivityBetweennessVariant Reverse4Order;
1063   qed;
1064 `;;
1065
1066 let HilbertAxiomRedundantByMoore = theorem `;
1067   ∀A B C D l.  Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ D ∈ l  ⇒
1068     ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D)
1069    ⇒  ordered D A B C ∨ ordered A D B C ∨ ordered A B D C ∨ ordered A B C D ∨
1070        ordered D A C B ∨ ordered A D C B ∨ ordered A C D B ∨ ordered A C B D ∨
1071        ordered D C A B ∨ ordered C D A B ∨ ordered C A D B ∨ ordered C A B D
1072
1073   proof
1074     intro_TAC ∀A B C D l, H1, H2;
1075     Collinear A B C     [] by fol H1 Collinear_DEF;
1076     B ∈ Open (A, C)  ∨  C ∈ Open (A, B)  ∨  A ∈ Open (C, B)     [] by fol H2 - B3' B1';
1077     fol - H1 H2 FourPointsOrder;
1078   qed;
1079 `;;
1080
1081 let InteriorTransitivity = theorem `;
1082   ∀A O B M G.  G ∈ int_angle A O B  ∧  M ∈ int_angle A O G
1083    ⇒  M ∈ int_angle A O B
1084
1085   proof
1086     intro_TAC ∀A O B M G, GintAOB MintAOG;
1087     ¬Collinear A O B     [AOBncol] by fol GintAOB IN_InteriorAngle;
1088     consider G' such that
1089     G' ∈ Open (A, B)  ∧  G' ∈ ray O G ━ {O}     [CrossG] by fol GintAOB Crossbar_THM;
1090     M ∈ int_angle A O G'     [] by fol MintAOG - InteriorWellDefined;
1091     consider M' such that
1092     M' ∈ Open (A, G')  ∧  M' ∈ ray O M ━ {O}     [CrossM] by fol - Crossbar_THM;
1093     ¬(M' = O) ∧ ¬(M = O) ∧ Collinear O M M' ∧ O ∉ Open (M', M)     [] by fol - IN_Ray IN_DIFF IN_SING;
1094     M ∈ ray O M' ━ {O}     [MrOM'] by fol - CollinearSymmetry B1' ∉ IN_Ray IN_DIFF IN_SING;
1095     Open (A, G') ⊂ Open (A, B)  ∧  M' ∈ Open (A, B)     [] by fol CrossG IntervalsAreConvex CrossM SUBSET;
1096     M' ∈ int_angle A O B     [] by fol AOBncol - ConverseCrossbar;
1097     fol - MrOM' WholeRayInterior;
1098   qed;
1099 `;;
1100
1101 let HalfPlaneConvexNonempty = theorem `;
1102   ∀l H A.  Line l ∧ A ∉ l  ⇒  H = {X | X ∉ l  ∧  X,A same_side l}
1103     ⇒  ¬(H = ∅)  ∧  H ⊂ complement l  ∧  Convex H
1104
1105   proof
1106     intro_TAC ∀l H A, l_line, HalfPlane;
1107     ∀X. X ∈ H  ⇔  X ∉ l  ∧  X,A same_side l     [Hdef] by simplify HalfPlane IN_ELIM_THM;
1108     H ⊂ complement l     [Hsub] by fol - IN_PlaneComplement SUBSET;
1109     A,A same_side l  ∧  A ∈ H     [] by fol l_line SameSideReflexive Hdef;
1110     ¬(H = ∅)     [Hnonempty] by fol - MEMBER_NOT_EMPTY;
1111     ∀P Q X.  P ∈ H ∧ Q ∈ H ∧ X ∈ Open (P, Q)  ⇒  X ∈ H     []
1112     proof
1113       intro_TAC ∀P Q X, PXQ;
1114       P ∉ l  ∧  P,A same_side l  ∧  Q ∉ l  ∧  Q,A same_side l     [PQinH] by fol - Hdef;
1115       P,Q same_side l     [Psim_lQ] by fol l_line - SameSideSymmetric SameSideTransitive;
1116       X ∉ l     [notXl] by fol - PXQ SameSide_DEF ∉;
1117       Open (X, P) ⊂ Open (P, Q)     [] by fol PXQ IntervalsAreConvex B1' SUBSET;
1118       X,P same_side l     [] by fol l_line - SUBSET Psim_lQ SameSide_DEF;
1119       X,A same_side l     [] by fol l_line notXl PQinH - Psim_lQ PQinH SameSideTransitive;
1120       fol - notXl Hdef;
1121     qed;
1122     fol Hnonempty Hsub - SUBSET CONVEX;
1123   qed;
1124 `;;
1125
1126 let PlaneSeparation = theorem `;
1127   ∀l.  Line l
1128    ⇒  ∃H1 H2. H1 ∩ H2 = ∅  ∧  ¬(H1 = ∅)  ∧  ¬(H2 = ∅)  ∧
1129          Convex H1  ∧  Convex H2  ∧  complement l = H1 ∪ H2  ∧
1130          ∀P Q. P ∈ H1 ∧ Q ∈ H2  ⇒  ¬(P,Q same_side l)
1131
1132   proof
1133     intro_TAC ∀l, l_line;
1134     consider A such that
1135     A ∉ l     [notAl] by fol l_line ExistsPointOffLine;
1136     consider E such that
1137     E ∈ l  ∧  ¬(A = E)     [El] by fol l_line I2 - ∉;
1138     consider B such that
1139     E ∈ Open (A, B)  ∧  ¬(E = B)  ∧  Collinear A E B     [AEB] by fol - B2' B1';
1140     B ∉ l     [notBl] by fol - l_line El ∉ notAl NonCollinearRaa CollinearSymmetry;
1141     ¬(A,B same_side l)     [Ansim_lB] by fol l_line El AEB SameSide_DEF;
1142     consider H1 H2 such that
1143     H1 = {X | X ∉ l  ∧  X,A same_side l}  ∧
1144     H2 = {X | X ∉ l  ∧  X,B same_side l}     [H12sets] by fol;
1145     ∀X. (X ∈ H1  ⇔  X ∉ l ∧ X,A same_side l) ∧
1146          (X ∈ H2  ⇔  X ∉ l ∧ X,B same_side l)     [H12def] by simplify IN_ELIM_THM -;
1147     H1 ∩ H2 = ∅     [H12disjoint]
1148     proof
1149       assume ¬(H1 ∩ H2 = ∅)     [nonempty] by fol;
1150       consider V such that
1151       V ∈ H1 ∧ V ∈ H2     [VinH12] by fol - MEMBER_NOT_EMPTY IN_INTER;
1152       V ∉ l  ∧  V,A same_side l  ∧  V ∉ l  ∧  V,B same_side l     [] by fol - H12def;
1153       A,B same_side l     [] by fol l_line - notAl notBl SameSideSymmetric SameSideTransitive;
1154       fol - Ansim_lB;
1155     qed;
1156     ¬(H1 = ∅) ∧ ¬(H2 = ∅) ∧ H1 ⊂ complement l ∧ H2 ⊂ complement l ∧
1157     Convex H1 ∧ Convex H2     [H12convex_nonempty] by fol l_line notAl notBl H12sets HalfPlaneConvexNonempty;
1158     H1 ∪ H2  ⊂  complement l     [H12sub] by fol H12convex_nonempty UNION_SUBSET;
1159     ∀C. C ∈ complement l  ⇒  C ∈ H1 ∪ H2     []
1160     proof
1161       intro_TAC ∀C, compl;
1162       C ∉ l     [notCl] by fol - IN_PlaneComplement;
1163       C,A same_side l  ∨  C,B same_side l     [] by fol l_line notAl notBl - Ansim_lB AtMost2Sides;
1164       fol notCl - H12def IN_UNION;
1165     qed;
1166     complement l  ⊂  H1 ∪ H2     [] by fol - SUBSET;
1167     complement l  =  H1 ∪ H2     [compl_H1unionH2] by fol H12sub - SUBSET_ANTISYM;
1168     ∀P Q. P ∈ H1 ∧ Q ∈ H2  ⇒  ¬(P,Q same_side l)     [opp_sides]
1169     proof
1170       intro_TAC ∀P Q, both;
1171       P ∉ l  ∧  P,A same_side l  ∧   Q ∉ l  ∧  Q,B same_side l     [PH1_QH2] by fol - H12def IN;
1172       fol l_line - notAl SameSideSymmetric notBl Ansim_lB SameSideTransitive;
1173     qed;
1174     fol H12disjoint H12convex_nonempty compl_H1unionH2 opp_sides;
1175   qed;
1176 `;;
1177
1178 let TetralateralSymmetry = theorem `;
1179   ∀A B C D.  Tetralateral A B C D
1180     ⇒  Tetralateral B C D A ∧ Tetralateral A B D C
1181
1182   proof
1183     intro_TAC ∀A B C D, H1;
1184     ¬Collinear A B D ∧ ¬Collinear B D C ∧ ¬Collinear D C A ∧ ¬Collinear C A B      [TetraABCD] by fol H1 Tetralateral_DEF CollinearSymmetry;
1185     simplify H1 - Tetralateral_DEF;
1186     fol H1 Tetralateral_DEF;
1187   qed;
1188 `;;
1189
1190 let EasyEmptyIntersectionsTetralateralHelp = theorem `;
1191   ∀A B C D. Tetralateral A B C D  ⇒  Open (A, B) ∩ Open (B, C) = ∅
1192
1193   proof
1194     intro_TAC ∀A B C D, H1;
1195     ∀X. X ∈ Open (B, C)  ⇒  X ∉ Open (A, B)     []
1196     proof
1197       intro_TAC ∀X, BXC;
1198       ¬Collinear A B C ∧ Collinear B X C ∧ ¬(X = B)     [] by fol H1 Tetralateral_DEF - B1';
1199       ¬Collinear A X B     [] by fol - CollinearSymmetry B1' NoncollinearityExtendsToLine;
1200       fol - B1' ∉;
1201     qed;
1202     fol - DisjointOneNotOther;
1203   qed;
1204 `;;
1205
1206 let EasyEmptyIntersectionsTetralateral = theorem `;
1207   ∀A B C D. Tetralateral A B C D
1208    ⇒  Open (A, B) ∩ Open (B, C) = ∅  ∧  Open (B, C) ∩ Open (C, D) = ∅  ∧
1209        Open (C, D) ∩ Open (D, A) = ∅  ∧  Open (D, A) ∩ Open (A, B) = ∅
1210
1211   proof
1212     intro_TAC ∀A B C D, H1;
1213     Tetralateral B C D A  ∧ Tetralateral C D A B  ∧ Tetralateral D A B C     [] by fol H1 TetralateralSymmetry;
1214     fol H1 - EasyEmptyIntersectionsTetralateralHelp;
1215   qed;
1216 `;;
1217
1218 let SegmentSameSideOppositeLine = theorem `;
1219   ∀A B C D a c.  Quadrilateral A B C D  ⇒
1220     Line a ∧ A ∈ a ∧ B ∈ a  ⇒  Line c ∧ C ∈ c ∧ D ∈ c
1221     ⇒  A,B same_side c  ∨  C,D same_side a
1222
1223   proof
1224     intro_TAC ∀A B C D a c, H1, a_line, c_line;
1225     assume ¬(C,D same_side a)     [CDnsim_a] by fol;
1226     consider G such that
1227     G ∈ a ∧ G ∈ Open (C, D)     [CGD] by fol - a_line SameSide_DEF;
1228     G ∈ c ∧ Collinear G B A     [Gc] by fol c_line - BetweenLinear a_line Collinear_DEF;
1229     ¬Collinear B C D  ∧  ¬Collinear C D A  ∧  Open (A, B) ∩ Open (C, D) = ∅     [quadABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF;
1230     A ∉ c ∧ B ∉ c ∧ ¬(A = G) ∧ ¬(B = G)     [Distinct] by fol - c_line Collinear_DEF ∉ Gc;
1231     G ∉ Open (A, B)     [] by fol quadABCD CGD DisjointOneNotOther;
1232     A ∈ ray G B ━ {G}      [] by fol Distinct Gc - IN_Ray IN_DIFF IN_SING;
1233     fol c_line Gc Distinct - RaySameSide;
1234   qed;
1235 `;;
1236
1237 let ConvexImpliesQuad = theorem `;
1238   ∀A B C D. Tetralateral A B C D  ⇒
1239     C ∈ int_angle D A B  ∧  D ∈ int_angle A B C
1240     ⇒  Quadrilateral A B C D
1241
1242   proof
1243     intro_TAC ∀A B C D, H1, H2;
1244     ¬(A = B) ∧ ¬(B = C) ∧ ¬(A = D)     [TetraABCD] by fol H1 Tetralateral_DEF;
1245     consider a such that
1246     Line a ∧ A ∈ a ∧ B ∈ a     [a_line] by fol TetraABCD I1;
1247     consider b such that
1248     Line b ∧ B ∈ b ∧ C ∈ b     [b_line] by fol TetraABCD I1;
1249     consider d such that
1250     Line d ∧ D ∈ d ∧ A ∈ d     [d_line] by fol TetraABCD I1;
1251     Open (B, C) ⊂ b  ∧  Open (A, B) ⊂ a     [BCbABa] by fol b_line a_line BetweenLinear SUBSET;
1252     D,A same_side b  ∧  C,D same_side a     [] by fol H2 a_line b_line d_line InteriorUse;
1253     b ∩ Open (D, A) = ∅  ∧  a ∩ Open (C, D) = ∅     [] by fol - b_line SameSide_DEF IN_INTER MEMBER_NOT_EMPTY;
1254     fol H1 BCbABa - INTER_TENSOR SUBSET_REFL SUBSET_EMPTY Quadrilateral_DEF;
1255   qed;
1256 `;;
1257
1258 let DiagonalsIntersectImpliesConvexQuad = theorem `;
1259   ∀A B C D G. ¬Collinear B C D  ⇒
1260     G ∈ Open (A, C)  ∧  G ∈ Open (B, D)
1261     ⇒  ConvexQuadrilateral A B C D
1262
1263   proof
1264     intro_TAC ∀A B C D G, BCDncol, DiagInt;
1265     ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D) ∧ ¬(C = A) ∧ ¬(A = G) ∧ ¬(D = G) ∧ ¬(B = G)     [Distinct] by fol BCDncol NonCollinearImpliesDistinct DiagInt B1';
1266     Collinear A G C ∧ Collinear B G D     [Gcols] by fol DiagInt B1';
1267     ¬Collinear C D G ∧ ¬Collinear B C G     [Gncols] by fol BCDncol CollinearSymmetry Distinct Gcols  NoncollinearityExtendsToLine;
1268     ¬Collinear C D A     [CDAncol] by fol - CollinearSymmetry Distinct Gcols  NoncollinearityExtendsToLine;
1269     ¬Collinear A B C ∧ ¬Collinear D A G     [ABCncol] by fol Gncols - CollinearSymmetry Distinct Gcols NoncollinearityExtendsToLine;
1270     ¬Collinear D A B     [DABncol] by fol - CollinearSymmetry Distinct Gcols NoncollinearityExtendsToLine;
1271     ¬(A = B) ∧ ¬(A = D)     [] by fol DABncol NonCollinearImpliesDistinct;
1272     Tetralateral A B C D     [TetraABCD] by fol Distinct - BCDncol CDAncol DABncol ABCncol Tetralateral_DEF;
1273     A ∈ ray C G ━ {C}  ∧  B ∈ ray D G ━ {D}  ∧  C ∈ ray A G ━ {A}  ∧  D ∈ ray B G ━ {B}     [ArCG] by fol DiagInt B1' IntervalRayEZ;
1274     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 fol BCDncol CDAncol DABncol ABCncol DiagInt B1' ConverseCrossbar;
1275     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 fol - ArCG WholeRayInterior;
1276     fol TetraABCD - ConvexImpliesQuad ConvexQuad_DEF;
1277   qed;
1278 `;;
1279
1280 let DoubleNotSimImpliesDiagonalsIntersect = theorem `;
1281   ∀A B C D l m.  Line l ∧ A ∈ l ∧ C ∈ l  ⇒  Line m ∧ B ∈ m ∧ D ∈ m  ⇒
1282     Tetralateral A B C D  ⇒  ¬(B,D same_side l)  ⇒  ¬(A,C same_side m)
1283     ⇒  (∃G. G ∈ Open (A, C) ∩ Open (B, D)) ∧ ConvexQuadrilateral A B C D
1284
1285   proof
1286     intro_TAC ∀A B C D l m, l_line, m_line, H1, H2, H3;
1287     ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B     [TetraABCD] by fol H1 Tetralateral_DEF;
1288     consider G such that
1289     G ∈ Open (A, C) ∧ G ∈ m     [AGC] by fol H3 m_line SameSide_DEF;
1290     G ∈ l     [Gl] by fol l_line - BetweenLinear;
1291     A ∉ m ∧ B ∉ l ∧ D ∉ l     [] by fol TetraABCD m_line l_line Collinear_DEF ∉;
1292     ¬(l = m) ∧ B ∈ m ━ {G} ∧ D ∈ m ━ {G}     [BDm_G] by fol - l_line ∉ m_line Gl IN_DIFF IN_SING;
1293     l ∩ m = {G}     [] by fol l_line m_line - Gl AGC I1Uniqueness;
1294     G ∈ Open (B, D)     [] by fol l_line m_line - BDm_G H2 EquivIntersection ∉;
1295     fol AGC - IN_INTER TetraABCD DiagonalsIntersectImpliesConvexQuad;
1296   qed;
1297 `;;
1298
1299 let ConvexQuadImpliesDiagonalsIntersect = theorem `;
1300   ∀A B C D l m.  Line l ∧ A ∈ l ∧ C ∈ l  ⇒  Line m ∧ B ∈ m ∧ D ∈ m  ⇒
1301     ConvexQuadrilateral A B C D
1302     ⇒  ¬(B,D same_side l) ∧ ¬(A,C same_side m) ∧
1303        (∃G. G ∈ Open (A, C) ∩ Open (B, D)) ∧ ¬Quadrilateral A B D C
1304
1305   proof
1306     intro_TAC ∀A B C D l m, l_line, m_line, ConvQuadABCD;
1307     Tetralateral A B C D ∧ A ∈ int_angle B C D ∧ D ∈ int_angle A B C     [convquadABCD] by fol ConvQuadABCD ConvexQuad_DEF Quadrilateral_DEF;
1308     ¬(B,D same_side l)  ∧  ¬(A,C same_side m)     [opp_sides] by fol convquadABCD l_line m_line InteriorOpposite;
1309     consider G such that
1310     G ∈ Open (A, C) ∩ Open (B, D)     [Gexists] by fol l_line m_line convquadABCD opp_sides DoubleNotSimImpliesDiagonalsIntersect;
1311     ¬(Open (B, D) ∩ Open (C, A) = ∅)     [] by fol - IN_INTER B1' MEMBER_NOT_EMPTY;
1312     ¬Quadrilateral A B D C     [] by fol - Quadrilateral_DEF;
1313     fol opp_sides Gexists -;
1314   qed;
1315 `;;
1316
1317 let FourChoicesTetralateralHelp = theorem `;
1318   ∀A B C D. Tetralateral A B C D  ∧  C ∈ int_angle D A B
1319     ⇒  ConvexQuadrilateral A B C D ∨ C ∈ int_triangle D A B
1320
1321   proof
1322     intro_TAC ∀A B C D, H1 CintDAB;
1323     ¬(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 fol H1 Tetralateral_DEF;
1324     consider a d such that
1325     Line a ∧ A ∈ a ∧ B ∈ a  ∧
1326     Line d ∧ D ∈ d ∧ A ∈ d     [ad_line] by fol TetraABCD I1;
1327     consider l m such that
1328     Line l ∧ A ∈ l ∧ C ∈ l  ∧
1329     Line m ∧ B ∈ m ∧ D ∈ m     [lm_line] by fol TetraABCD I1;
1330     C ∉ a ∧ C ∉ d ∧ B ∉ l ∧ D ∉ l ∧ A ∉ m ∧ C ∉ m ∧ ¬Collinear A B D ∧ ¬Collinear B D A          [tetra'] by fol TetraABCD ad_line lm_line Collinear_DEF ∉ CollinearSymmetry;
1331     ¬(B,D same_side l)     [Bsim_lD] by fol CintDAB lm_line InteriorOpposite - SameSideSymmetric;
1332     assume A,C same_side m     [same] by fol lm_line H1 Bsim_lD DoubleNotSimImpliesDiagonalsIntersect;
1333     C,A same_side m     [Csim_mA] by fol lm_line - tetra' SameSideSymmetric;
1334     C,B same_side d  ∧  C,D same_side a     [] by fol ad_line CintDAB InteriorUse;
1335     C ∈ int_angle A B D  ∧  C ∈ int_angle B D A     [] by fol tetra' ad_line lm_line Csim_mA - IN_InteriorAngle;
1336     fol CintDAB - IN_InteriorTriangle;
1337   qed;
1338 `;;
1339
1340 let FourChoicesTetralateralHelp = theorem `;
1341   ∀A B C D. Tetralateral A B C D  ∧  C ∈ int_angle D A B
1342     ⇒  ConvexQuadrilateral A B C D ∨ C ∈ int_triangle D A B
1343
1344   proof
1345     intro_TAC ∀A B C D, H1 CintDAB;
1346     ¬(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 fol H1 Tetralateral_DEF;
1347     consider a d such that
1348     Line a ∧ A ∈ a ∧ B ∈ a  ∧
1349     Line d ∧ D ∈ d ∧ A ∈ d     [ad_line] by fol TetraABCD I1;
1350     consider l m such that
1351     Line l ∧ A ∈ l ∧ C ∈ l  ∧
1352     Line m ∧ B ∈ m ∧ D ∈ m     [lm_line] by fol TetraABCD I1;
1353     C ∉ a ∧ C ∉ d ∧ B ∉ l ∧ D ∉ l ∧ A ∉ m ∧ C ∉ m ∧ ¬Collinear A B D ∧ ¬Collinear B D A          [tetra'] by fol TetraABCD ad_line lm_line Collinear_DEF ∉ CollinearSymmetry;
1354     ¬(B,D same_side l)     [Bsim_lD] by fol CintDAB lm_line InteriorOpposite - SameSideSymmetric;
1355     assume A,C same_side m     [same] by fol lm_line H1 Bsim_lD  DoubleNotSimImpliesDiagonalsIntersect;
1356     C,A same_side m     [Csim_mA] by fol lm_line - tetra' SameSideSymmetric;
1357     C,B same_side d  ∧  C,D same_side a     [] by fol ad_line CintDAB InteriorUse;
1358     C ∈ int_angle A B D  ∧  C ∈ int_angle B D A     [] by fol tetra' ad_line lm_line Csim_mA - IN_InteriorAngle;
1359     fol CintDAB - IN_InteriorTriangle;
1360   qed;
1361 `;;
1362
1363 let InteriorTriangleSymmetry = theorem `;
1364   ∀A B C P. P ∈ int_triangle A B C  ⇒ P ∈ int_triangle B C A
1365   by fol IN_InteriorTriangle`;;
1366
1367 let FourChoicesTetralateral = theorem `;
1368   ∀A B C D a. Tetralateral A B C D  ⇒
1369     Line a ∧ A ∈ a ∧ B ∈ a  ⇒  C,D same_side a
1370     ⇒  ConvexQuadrilateral A B C D  ∨  ConvexQuadrilateral A B D C  ∨
1371        D ∈ int_triangle A B C  ∨  C ∈ int_triangle D A B
1372
1373   proof
1374     intro_TAC ∀A B C D a, H1, a_line, Csim_aD;
1375      ¬(A = B) ∧ ¬Collinear A B C ∧ ¬Collinear C D A ∧ ¬Collinear D A B ∧ Tetralateral A B D C     [TetraABCD] by fol H1 Tetralateral_DEF TetralateralSymmetry;
1376     ¬Collinear C A D ∧ C ∉ a ∧ D ∉ a     [notCDa] by fol TetraABCD CollinearSymmetry a_line Collinear_DEF ∉;
1377     C ∈ int_angle D A B  ∨  D ∈ int_angle C A B     [] by fol TetraABCD a_line - Csim_aD AngleOrdering;
1378     case_split CintDAB | DintCAB     by fol -;
1379     suppose C ∈ int_angle D A B;
1380       ConvexQuadrilateral A B C D  ∨  C ∈ int_triangle D A B     [] by fol H1 - FourChoicesTetralateralHelp;
1381       fol -;
1382     end;
1383     suppose D ∈ int_angle C A B;
1384       ConvexQuadrilateral A B D C  ∨  D ∈ int_triangle C A B     [] by fol TetraABCD - FourChoicesTetralateralHelp;
1385       fol - InteriorTriangleSymmetry;
1386     end;
1387   qed;
1388 `;;
1389
1390 let QuadrilateralSymmetry = theorem `;
1391   ∀A B C D. Quadrilateral A B C D  ⇒
1392     Quadrilateral B C D A  ∧  Quadrilateral C D A B  ∧  Quadrilateral D A B C
1393   by fol Quadrilateral_DEF INTER_COMM TetralateralSymmetry Quadrilateral_DEF`;;
1394
1395 let FiveChoicesQuadrilateral = theorem `;
1396   ∀A B C D l m.  Quadrilateral A B C D  ⇒
1397     Line l ∧ A ∈ l ∧ C ∈ l  ∧  Line m ∧ B ∈ m ∧ D ∈ m
1398     ⇒  (ConvexQuadrilateral A B C D  ∨  A ∈ int_triangle B C D  ∨
1399        B ∈ int_triangle C D A  ∨  C ∈ int_triangle D A B  ∨
1400        D ∈ int_triangle A B C)  ∧
1401        (¬(B,D same_side l) ∨ ¬(A,C same_side m))
1402
1403   proof
1404     intro_TAC ∀A B C D l m, H1, lm_line;
1405     Tetralateral A B C D     [H1Tetra] by fol H1 Quadrilateral_DEF;
1406     ¬(A = B) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(C = D)     [Distinct] by fol H1Tetra Tetralateral_DEF;
1407     consider a c such that
1408     Line a ∧ A ∈ a ∧ B ∈ a  ∧
1409     Line c ∧ C ∈ c ∧ D ∈ c     [ac_line] by fol Distinct I1;
1410     Quadrilateral C D A B  ∧  Tetralateral C D A B     [tetraCDAB] by fol H1 QuadrilateralSymmetry Quadrilateral_DEF;
1411     ¬ConvexQuadrilateral A B D C  ∧  ¬ConvexQuadrilateral C D B A     [notconvquad] by fol Distinct I1 H1 - ConvexQuadImpliesDiagonalsIntersect;
1412     ConvexQuadrilateral A B C D  ∨  A ∈ int_triangle B C D  ∨
1413     B ∈ int_triangle C D A  ∨  C ∈ int_triangle D A B  ∨
1414     D ∈ int_triangle A B C     [5choices]
1415     proof
1416       A,B same_side c  ∨  C,D same_side a     [2pos] by fol H1 ac_line SegmentSameSideOppositeLine;
1417       assume A,B same_side c     [Asym_cB] by fol 2pos H1Tetra ac_line notconvquad FourChoicesTetralateral;
1418       ConvexQuadrilateral C D A B  ∨  B ∈ int_triangle C D A  ∨
1419       A ∈ int_triangle B C D     [X1] by fol tetraCDAB ac_line - notconvquad FourChoicesTetralateral;
1420       fol - QuadrilateralSymmetry ConvexQuad_DEF;
1421     qed;
1422     ¬(B,D same_side l) ∨ ¬(A,C same_side m)     [] by fol - lm_line ConvexQuadImpliesDiagonalsIntersect IN_InteriorTriangle InteriorAngleSymmetry InteriorOpposite;
1423     fol 5choices -;
1424   qed;
1425 `;;
1426
1427 let IntervalSymmetry = theorem `;
1428   ∀A B. Open (A, B) = Open (B, A)
1429   by fol B1' EXTENSION`;;
1430
1431 let SegmentSymmetry = theorem `;
1432   ∀A B. seg A B = seg B A
1433   by fol Segment_DEF INSERT_COMM IntervalSymmetry`;;
1434
1435 let C1OppositeRay = theorem `;
1436   ∀O P s.  Segment s ∧ ¬(O = P)  ⇒  ∃Q. P ∈ Open (O, Q)  ∧  seg P Q ≡ s
1437
1438   proof
1439     intro_TAC ∀O P s, H1;
1440     consider Z such that
1441     P ∈ Open (O, Z)  ∧  ¬(P = Z)     [OPZ] by fol H1 B2' B1';
1442     consider Q such that
1443     Q ∈ ray P Z ━ {P} ∧ seg P Q ≡ s     [PQeq] by fol H1 - C1;
1444     P ∈ Open (Q, O)     [] by fol OPZ - OppositeRaysIntersect1pointHelp;
1445     fol - B1' PQeq;
1446   qed;
1447 `;;
1448
1449 let OrderedCongruentSegments = theorem `;
1450   ∀A B C D G.  ¬(A = C) ∧ ¬(D = G)  ⇒  seg A C ≡ seg D G  ⇒  B ∈ Open (A, C)
1451     ⇒  ∃E. E ∈ Open (D, G)  ∧  seg A B ≡ seg D E
1452
1453   proof
1454     intro_TAC ∀A B C D G, H1, H2, H3;
1455     Segment (seg A B) ∧ Segment (seg A C) ∧ Segment (seg B C) ∧ Segment (seg D G)     [segs] by fol H3 B1' H1 SEGMENT;
1456     seg D G ≡ seg A C     [DGeqAC] by fol - H2 C2Symmetric;
1457     consider E such that
1458     E ∈ ray D G ━ {D} ∧ seg D E ≡ seg A B     [DEeqAB] by fol segs H1 C1;
1459     ¬(E = D) ∧ Collinear D E G ∧ D ∉ Open (G, E)     [ErDG] by fol - IN_DIFF IN_SING IN_Ray B1' CollinearSymmetry ∉;
1460     consider G' such that
1461     E ∈ Open (D, G') ∧ seg E G' ≡ seg B C     [DEG'] by fol segs - C1OppositeRay;
1462     seg D G' ≡ seg A C     [DG'eqAC] by fol DEG' H3 DEeqAB C3;
1463     Segment (seg D G') ∧ Segment (seg D E)     [] by fol DEG' B1' SEGMENT;
1464     seg A C ≡ seg D G' ∧ seg A B ≡ seg D E     [ABeqDE] by fol segs - DG'eqAC C2Symmetric DEeqAB;
1465     G' ∈ ray D E ━ {D}  ∧  G ∈ ray D E ━ {D}     [] by fol DEG' IntervalRayEZ ErDG IN_Ray H1 IN_DIFF IN_SING;
1466     G' = G     [] by fol ErDG segs - DG'eqAC DGeqAC C1;
1467     fol - DEG' ABeqDE;
1468   qed;
1469 `;;
1470
1471 let SegmentSubtraction = theorem `;
1472   ∀A B C A' B' C'. B ∈ Open (A, C)  ∧  B' ∈ Open (A', C')  ⇒
1473     seg A B ≡ seg A' B'  ⇒  seg A C ≡ seg A' C'
1474     ⇒  seg B C ≡ seg B' C'
1475
1476   proof
1477     intro_TAC ∀A B C A' B' C', H1, H2, H3;
1478     ¬(A = B) ∧ ¬(A = C) ∧ Collinear A B C ∧ Segment (seg A' C') ∧ Segment (seg B' C')     [Distinct] by fol H1 B1' SEGMENT;
1479     consider Q such that
1480     B ∈ Open (A, Q)  ∧  seg B Q ≡ seg B' C'     [defQ] by fol - C1OppositeRay;
1481     seg A Q ≡ seg A' C'     [AQ_A'C'] by fol H1 H2 - C3;
1482     ¬(A = Q)  ∧  Collinear A B Q  ∧  A ∉ Open (C, B)  ∧  A ∉ Open (Q, B)     []
1483     proof     simplify defQ B1' ∉;     fol defQ B1' H1 B3';     qed;
1484     C ∈ ray A B ━ {A}  ∧  Q ∈ ray A B ━ {A}     [] by fol Distinct - IN_Ray IN_DIFF IN_SING;
1485     fol defQ Distinct - AQ_A'C' H3 C1;
1486   qed;
1487 `;;
1488
1489 let SegmentOrderingUse = theorem `;
1490   ∀A B s.  Segment s  ∧  ¬(A = B)  ⇒  s <__ seg A B
1491     ⇒  ∃G. G ∈ Open (A, B)  ∧  s ≡ seg A G
1492
1493   proof
1494     intro_TAC ∀A B s, H1, H2;
1495     consider A' B' G' such that
1496     seg A B = seg A' B'  ∧  G' ∈ Open (A', B')  ∧  s ≡ seg A' G'     [H2'] by fol H2 SegmentOrdering_DEF;
1497     ¬(A' = G') ∧ ¬(A' = B')  ∧  seg A' B' ≡ seg A B     [A'notB'G'] by fol - B1' H1 SEGMENT C2Reflexive;
1498     consider G such that
1499     G ∈ Open (A, B)  ∧  seg A' G' ≡ seg A G     [AGB] by fol A'notB'G' H1 H2' -  OrderedCongruentSegments;
1500     s ≡ seg A G     [] by fol H1 A'notB'G' - B1' SEGMENT H2' C2Transitive;
1501     fol AGB -;
1502   qed;
1503 `;;
1504
1505 let SegmentTrichotomy1 = theorem `;
1506   ∀s t.  s <__ t  ⇒  ¬(s ≡ t)
1507
1508   proof
1509     intro_TAC ∀s t, H1;
1510     consider A B G such that
1511     Segment s ∧ t = seg A B ∧ G ∈ Open (A, B) ∧ s ≡ seg A G     [H1'] by fol H1 SegmentOrdering_DEF;
1512     ¬(A = G) ∧ ¬(A = B) ∧ ¬(G = B)     [Distinct] by fol H1' B1';
1513     seg A B ≡ seg A B     [ABrefl] by fol - SEGMENT C2Reflexive;
1514     G ∈ ray A B ━ {A}  ∧  B ∈ ray A B ━ {A}     [] by fol H1' IntervalRay EndpointInRay Distinct IN_DIFF IN_SING;
1515     ¬(seg A G ≡ seg A B)  ∧ seg A G ≡ s     [] by fol Distinct SEGMENT - ABrefl C1 H1' C2Symmetric;
1516     fol Distinct H1' SEGMENT - C2Transitive;
1517   qed;
1518 `;;
1519
1520 let SegmentTrichotomy2 = theorem `;
1521   ∀s t u.  s <__ t  ∧  Segment u  ∧  t ≡ u  ⇒  s <__ u
1522
1523   proof
1524     intro_TAC ∀s t u, H1 H2;
1525     consider A B P such that
1526     Segment s  ∧  t = seg A B  ∧  P ∈ Open (A, B)  ∧  s ≡ seg A P     [H1'] by fol H1 SegmentOrdering_DEF;
1527     ¬(A = B) ∧ ¬(A = P)     [Distinct] by fol - B1';
1528     consider X Y such that
1529     u = seg X Y ∧ ¬(X = Y)     [uXY] by fol H2 SEGMENT;
1530     consider Q such that
1531     Q ∈ Open (X, Y)  ∧  seg A P ≡ seg X Q     [XQY] by fol Distinct - H1' H2 OrderedCongruentSegments;
1532     ¬(X = Q)  ∧  s ≡ seg X Q     [] by fol - B1' H1' Distinct SEGMENT XQY C2Transitive;
1533     fol H1' uXY XQY - SegmentOrdering_DEF;
1534   qed;
1535 `;;
1536
1537 let SegmentOrderTransitivity = theorem `;
1538   ∀s t u.  s <__ t  ∧  t <__ u  ⇒  s <__ u
1539
1540   proof
1541     intro_TAC ∀s t u, H1;
1542     consider A B G such that
1543     u = seg A B  ∧  G ∈ Open (A, B)  ∧  t ≡ seg A G     [H1'] by fol H1 SegmentOrdering_DEF;
1544     ¬(A = B) ∧ ¬(A = G) ∧ Segment s     [Distinct] by fol H1'  B1' H1 SegmentOrdering_DEF;
1545     s <__ seg A G     [] by fol H1 H1' Distinct SEGMENT SegmentTrichotomy2;
1546     consider F such that
1547     F ∈ Open (A, G) ∧ s ≡ seg A F     [AFG] by fol Distinct - SegmentOrderingUse;
1548     F ∈ Open (A, B)     [] by fol H1' IntervalsAreConvex - SUBSET;
1549     fol Distinct H1' - AFG SegmentOrdering_DEF;
1550   qed;
1551 `;;
1552
1553 let SegmentTrichotomy = theorem `;
1554   ∀s t.  Segment s ∧ Segment t
1555     ⇒  (s ≡ t  ∨  s <__ t  ∨  t <__ s)  ∧  ¬(s ≡ t ∧ s <__ t)  ∧
1556        ¬(s ≡ t ∧ t <__ s)  ∧  ¬(s <__ t ∧ t <__ s)
1557
1558   proof
1559     intro_TAC ∀s t, H1;
1560     ¬(s ≡ t  ∧  s <__ t)     [Not12] by fol - SegmentTrichotomy1;
1561     ¬(s ≡ t  ∧  t <__ s)     [Not13] by fol H1 - SegmentTrichotomy1 C2Symmetric;
1562     ¬(s <__ t  ∧  t <__ s)     [Not23] by fol H1 - SegmentOrderTransitivity SegmentTrichotomy1 H1 C2Reflexive;
1563     consider O P such that
1564     s = seg O P  ∧  ¬(O = P)     [sOP] by fol H1 SEGMENT;
1565     consider Q such that
1566     Q ∈ ray O P ━ {O}  ∧  seg O Q ≡ t     [QrOP] by fol H1 - C1;
1567     O ∉ Open (Q, P)  ∧  Collinear O P Q   ∧  ¬(O = Q)     [notQOP] by fol - IN_DIFF IN_SING IN_Ray;
1568     s ≡ seg O P  ∧  t ≡ seg O Q  ∧  seg O Q ≡ t  ∧  seg O P ≡ s     [stOPQ] by fol H1 sOP - SEGMENT QrOP C2Reflexive C2Symmetric;
1569     assume ¬(Q = P) [notQP] by fol stOPQ sOP QrOP Not12 Not13 Not23;
1570     P ∈ Open (O, Q)  ∨  Q ∈ Open (O, P)     [] by fol sOP - notQOP B3' B1' ∉;
1571     s <__ seg O Q  ∨  t <__ seg O P     [] by fol H1 - stOPQ SegmentOrdering_DEF;
1572     s <__ t  ∨  t <__ s     [] by fol - H1 stOPQ SegmentTrichotomy2;
1573     fol - Not12 Not13 Not23;
1574   qed;
1575 `;;
1576
1577
1578 let C4Uniqueness = theorem `;
1579   ∀O A B P l.  Line l ∧ O ∈ l ∧ A ∈ l ∧ ¬(O = A)  ⇒
1580     B ∉ l ∧ P ∉ l ∧ P,B same_side l  ⇒  ∡ A O P ≡ ∡ A O B
1581     ⇒  ray O B = ray O P
1582
1583   proof
1584     intro_TAC ∀O A B P l, H1, H2, H3;
1585     ¬(O = B) ∧ ¬(O = P) ∧ Ray (ray O B) ∧ Ray (ray O P)     [Distinct] by fol H2 H1 ∉ RAY;
1586     ¬Collinear A O B  ∧  B,B same_side l     [Bsim_lB] by fol H1 H2 I1 Collinear_DEF ∉ SameSideReflexive;
1587     Angle (∡ A O B)  ∧  ∡ A O B ≡ ∡ A O B     [] by fol - ANGLE C5Reflexive;
1588     fol - H1 H2 Distinct Bsim_lB H3 C4;
1589   qed;
1590 `;;
1591
1592 let AngleSymmetry = theorem `;
1593   ∀A O B. ∡ A O B = ∡ B O A
1594   by fol Angle_DEF UNION_COMM`;;
1595
1596 let TriangleCongSymmetry = theorem `;
1597   ∀A B C A' B' C'. A,B,C ≅ A',B',C'
1598    ⇒  A,C,B ≅ A',C',B' ∧ B,A,C ≅ B',A',C' ∧
1599        B,C,A ≅ B',C',A' ∧ C,A,B ≅ C',A',B' ∧ C,B,A ≅ C',B',A'
1600
1601   proof
1602     intro_TAC ∀A B C A' B' C', H1;
1603     ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
1604     seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧ seg B C ≡ seg B' C' ∧
1605     ∡ A B C ≡ ∡ A' B' C' ∧ ∡ B C A ≡ ∡ B' C' A' ∧ ∡ C A B ≡ ∡ C' A' B'     [H1'] by fol H1 TriangleCong_DEF;
1606     seg B A ≡ seg B' A' ∧ seg C A ≡ seg C' A' ∧ seg C B ≡ seg C' B'     [segments] by fol H1' SegmentSymmetry;
1607     ∡ C B A ≡ ∡ C' B' A' ∧ ∡ A C B ≡ ∡ A' C' B' ∧ ∡ B A C ≡ ∡ B' A' C'     [] by fol H1' AngleSymmetry;
1608     fol CollinearSymmetry H1' segments - TriangleCong_DEF;
1609   qed;
1610 `;;
1611
1612 let SAS = theorem `;
1613   ∀A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C'  ⇒
1614     seg B A ≡ seg B' A'  ∧  seg B C ≡ seg B' C'  ⇒ ∡ A B C ≡ ∡ A' B' C'
1615     ⇒  A,B,C ≅ A',B',C'
1616
1617   proof
1618     intro_TAC ∀A B C A' B' C', H1, H2, H3;
1619     ¬(A = B) ∧ ¬(A = C) ∧ ¬(A' = C')     [Distinct] by fol H1 NonCollinearImpliesDistinct;
1620     consider c such that
1621     Line c ∧ A ∈ c ∧ B ∈ c     [c_line] by fol Distinct I1;
1622     C ∉ c     [notCc] by fol H1 c_line Collinear_DEF ∉;
1623     ∡ B C A ≡ ∡ B' C' A'     [BCAeq] by fol H1 H2 H3 C6;
1624     ∡ B A C ≡ ∡ B' A' C'     [BACeq] by fol H1 CollinearSymmetry H2 H3 AngleSymmetry C6;
1625     consider Y such that
1626     Y ∈ ray A C ━ {A}  ∧  seg A Y ≡ seg A' C'     [YrAC] by fol Distinct SEGMENT C1;
1627     Y ∉ c  ∧  Y,C same_side c     [Ysim_cC] by fol c_line notCc - RaySameSide;
1628     ¬Collinear Y A B     [YABncol] by fol Distinct c_line - NonCollinearRaa CollinearSymmetry;
1629     ray A Y = ray A C  ∧  ∡ Y A B = ∡ C A B     [] by fol Distinct YrAC RayWellDefined Angle_DEF;
1630     ∡ Y A B ≡ ∡ C' A' B'     [] by fol BACeq - AngleSymmetry;
1631     ∡ A B Y ≡ ∡ A' B' C'     [ABYeq] by fol YABncol H1 CollinearSymmetry H2 SegmentSymmetry YrAC - C6;
1632     Angle (∡ A B C) ∧ Angle (∡ A' B' C') ∧ Angle (∡ A B Y)     [] by fol H1 CollinearSymmetry YABncol ANGLE;
1633     ∡ A B Y ≡ ∡ A B C     [ABYeqABC] by fol - ABYeq - H3 C5Symmetric C5Transitive;
1634     ray B C = ray B Y  ∧  ¬(Y = B)  ∧  Y ∈ ray B C     [] by fol c_line Distinct notCc Ysim_cC ABYeqABC C4Uniqueness ∉ - EndpointInRay;
1635     Collinear B C Y  ∧  Collinear A C Y     [ABCYcol] by fol - YrAC IN_DIFF IN_SING IN_Ray;
1636     C = Y     [] by fol H1 ABCYcol TwoSidesTriangle1Intersection;
1637     seg A C ≡ seg A' C'     [] by fol - YrAC;
1638     fol H1 H2 SegmentSymmetry - H3 BCAeq BACeq AngleSymmetry TriangleCong_DEF;
1639   qed;
1640 `;;
1641
1642 let ASA = theorem `;
1643   ∀A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C'  ⇒
1644     seg A C ≡ seg A' C'  ⇒  ∡ C A B ≡ ∡ C' A' B'  ∧  ∡ B C A ≡ ∡ B' C' A'
1645     ⇒  A,B,C ≅ A',B',C'
1646
1647   proof
1648     intro_TAC ∀A B C A' B' C', H1, H2, H3;
1649     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬(A' = B') ∧ ¬(A' = C') ∧ ¬(B' = C') ∧
1650     Segment (seg C' B')     [Distinct] by fol H1 NonCollinearImpliesDistinct SEGMENT;
1651     consider D such that
1652     D ∈ ray C B ━ {C}  ∧  seg C D ≡ seg C' B'  ∧  ¬(D = C)     [DrCB] by fol - C1 IN_DIFF IN_SING;
1653     Collinear C B D     [CBDcol] by fol - IN_DIFF IN_SING IN_Ray;
1654     ¬Collinear D C A ∧ Angle (∡ C A D) ∧ Angle (∡ C' A' B') ∧ Angle (∡ C A B)     [DCAncol] by fol H1 CollinearSymmetry - DrCB NoncollinearityExtendsToLine H1 ANGLE;
1655     consider b such that
1656     Line b ∧ A ∈ b ∧ C ∈ b     [b_line] by fol Distinct I1;
1657     B ∉ b ∧ ¬(D = A)     [notBb] by fol H1 - Collinear_DEF ∉ DCAncol NonCollinearImpliesDistinct;
1658     D ∉ b  ∧  D,B same_side b     [Dsim_bB] by fol b_line - DrCB RaySameSide;
1659     ray C D = ray C B     [] by fol Distinct DrCB RayWellDefined;
1660     ∡ D C A ≡ ∡ B' C' A'     [] by fol H3 - Angle_DEF;
1661     D,C,A ≅ B',C',A'     [] by fol DCAncol H1 CollinearSymmetry DrCB H2 SegmentSymmetry - SAS;
1662     ∡ C A D ≡ ∡ C' A' B'     [] by fol - TriangleCong_DEF;
1663     ∡ C A D ≡ ∡ C A B     [] by fol DCAncol - H3 C5Symmetric C5Transitive;
1664     ray A B = ray A D  ∧  D ∈ ray A B     [] by fol b_line Distinct notBb Dsim_bB - C4Uniqueness notBb EndpointInRay;
1665     Collinear A B D     [ABDcol] by fol - IN_Ray;
1666     D = B     [] by fol H1 CBDcol ABDcol CollinearSymmetry TwoSidesTriangle1Intersection;
1667     seg C B ≡ seg C' B'     [] by fol - DrCB;
1668     B,C,A ≅ B',C',A'     [] by fol H1 CollinearSymmetry - H2 SegmentSymmetry H3 SAS;
1669     fol - TriangleCongSymmetry;
1670   qed;
1671 `;;
1672
1673 let AngleSubtraction = theorem `;
1674   ∀A O B A' O' B' G G'. G ∈ int_angle A O B  ∧  G' ∈ int_angle A' O' B'  ⇒
1675     ∡ A O B ≡ ∡ A' O' B'  ∧  ∡ A O G ≡ ∡ A' O' G'
1676     ⇒  ∡ G O B ≡ ∡ G' O' B'
1677
1678   proof
1679     intro_TAC ∀A O B A' O' B' G G', H1, H2;
1680     ¬Collinear A O B ∧ ¬Collinear A' O' B'     [A'O'B'ncol] by fol H1 IN_InteriorAngle;
1681     ¬(A = O) ∧ ¬(O = B) ∧ ¬(G = O) ∧ ¬(G' = O') ∧ Segment (seg O' A') ∧ Segment (seg O' B')     [Distinct] by fol - NonCollinearImpliesDistinct H1 InteriorEZHelp SEGMENT;
1682    consider X Y such that
1683    X ∈ ray O A ━ {O}  ∧  seg O X ≡ seg O' A'  ∧  Y ∈ ray O B ━ {O}  ∧  seg O Y ≡ seg O' B'     [XYexists] by fol - C1;
1684     G ∈ int_angle X O Y     [GintXOY] by fol H1 XYexists InteriorWellDefined InteriorAngleSymmetry;
1685     consider H H' such that
1686     H ∈ Open (X, Y)  ∧  H ∈ ray O G ━ {O}  ∧
1687     H' ∈ Open (A', B')  ∧  H' ∈ ray O' G' ━ {O'}     [Hexists] by fol - H1 Crossbar_THM;
1688     H ∈ int_angle X O Y  ∧  H' ∈ int_angle A' O' B'     [HintXOY] by fol GintXOY H1 - WholeRayInterior;
1689     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 fol Distinct XYexists Hexists RayWellDefined;
1690     ∡ X O Y ≡ ∡ A' O' B'  ∧  ∡ X O H ≡ ∡ A' O' H'     [H2'] by fol H2 - Angle_DEF;
1691     ¬Collinear X O Y     [] by fol GintXOY IN_InteriorAngle;
1692     X,O,Y ≅ A',O',B'     [] by fol - A'O'B'ncol H2' XYexists SAS;
1693     seg X Y ≡ seg A' B'  ∧  ∡ O Y X ≡ ∡ O' B' A'  ∧  ∡ Y X O ≡ ∡ B' A' O'     [XOYcong] by fol - TriangleCong_DEF;
1694     ¬Collinear O H X ∧ ¬Collinear O' H' A' ∧ ¬Collinear O Y H ∧ ¬Collinear O' B' H'     [OHXncol] by fol HintXOY InteriorEZHelp InteriorAngleSymmetry CollinearSymmetry;
1695     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 fol Hexists B1' IntervalRay;
1696     ∡ H X O ≡ ∡ H' A' O'     [] by fol XOYcong - Angle_DEF;
1697     O,H,X ≅ O',H',A'     [] by fol OHXncol XYexists - H2' ASA;
1698     seg X H ≡ seg A' H'     [] by fol - TriangleCong_DEF SegmentSymmetry;
1699     seg H Y ≡ seg H' B'     [] by fol Hexists XOYcong - SegmentSubtraction;
1700     seg Y O  ≡ seg B' O'  ∧  seg Y H ≡ seg B' H'     [YHeq] by fol XYexists - SegmentSymmetry;
1701     ∡ O Y H ≡ ∡ O' B' H'     [] by fol XOYcong Hrays Angle_DEF;
1702     O,Y,H ≅ O',B',H'     [] by fol OHXncol YHeq - SAS;
1703   ∡ H O Y ≡ ∡ H' O' B'     [] by fol - TriangleCong_DEF;
1704   fol - Orays Angle_DEF;
1705   qed;
1706 `;;
1707
1708 let OrderedCongruentAngles = theorem `;
1709   ∀A O B A' O' B' G. ¬Collinear A' O' B'  ∧  ∡ A O B ≡ ∡ A' O' B'  ∧ G ∈ int_angle A O B
1710     ⇒  ∃G'. G' ∈ int_angle A' O' B'  ∧  ∡ A O G ≡ ∡ A' O' G'
1711
1712   proof
1713     intro_TAC ∀A O B A' O' B' G, H1 H2 H3;
1714     ¬Collinear A O B     [AOBncol] by fol H3 IN_InteriorAngle;
1715     ¬(A = O) ∧ ¬(O = B) ∧ ¬(A' = B') ∧ ¬(O = G) ∧ Segment (seg O' A') ∧ Segment (seg O' B')     [Distinct] by fol AOBncol H1 NonCollinearImpliesDistinct H3 InteriorEZHelp SEGMENT;
1716     consider X Y such that
1717     X ∈ ray O A ━ {O}  ∧  seg O X ≡ seg O' A'  ∧  Y ∈ ray O B ━ {O}  ∧  seg O Y ≡ seg O' B'     [defXY] by fol - C1;
1718     G ∈ int_angle X O Y     [GintXOY] by fol H3 - InteriorWellDefined InteriorAngleSymmetry;
1719     ¬Collinear X O Y ∧ ¬(X = Y)     [XOYncol] by fol - IN_InteriorAngle NonCollinearImpliesDistinct;
1720     consider H such that
1721     H ∈ Open (X, Y)  ∧  H ∈ ray O G ━ {O}     [defH] by fol GintXOY Crossbar_THM;
1722     ray O X = ray O A  ∧  ray O Y = ray O B  ∧  ray O H = ray O G     [Orays] by fol Distinct defXY - RayWellDefined;
1723     ∡ X O Y ≡ ∡ A' O' B'     [] by fol H2 - Angle_DEF;
1724     X,O,Y ≅ A',O',B'     [] by fol XOYncol H1 defXY - SAS;
1725     seg X Y ≡ seg A' B'  ∧  ∡ O X Y ≡ ∡ O' A' B'     [YXOcong] by fol - TriangleCong_DEF AngleSymmetry;
1726     consider G' such that
1727     G' ∈ Open (A', B')  ∧  seg X H ≡ seg A' G'     [A'G'B'] by fol XOYncol Distinct - defH OrderedCongruentSegments;
1728     G' ∈ int_angle A' O' B'     [G'intA'O'B'] by fol H1 - ConverseCrossbar;
1729     ray X H = ray X Y  ∧  ray A' G' = ray A' B'     [] by fol defH A'G'B' IntervalRay;
1730     ∡ O X H ≡ ∡ O' A' G'     [HXOeq] by fol - Angle_DEF YXOcong;
1731     H ∈ int_angle X O Y     [] by fol GintXOY defH WholeRayInterior;
1732     ¬Collinear O X H ∧ ¬Collinear O' A' G'     [] by fol - G'intA'O'B' InteriorEZHelp CollinearSymmetry;
1733     O,X,H ≅ O',A',G'     [] by fol - A'G'B' defXY SegmentSymmetry HXOeq SAS;
1734     ∡ X O H ≡ ∡ A' O' G'     [] by fol - TriangleCong_DEF AngleSymmetry;
1735     fol G'intA'O'B' - Orays Angle_DEF;
1736   qed;
1737 `;;
1738
1739 let AngleAddition = theorem `;
1740   ∀A O B A' O' B' G G'.  G ∈ int_angle A O B  ∧  G' ∈ int_angle A' O' B'  ⇒
1741     ∡ A O G ≡ ∡ A' O' G'  ∧  ∡ G O B ≡ ∡ G' O' B'
1742    ⇒  ∡ A O B ≡ ∡ A' O' B'
1743
1744   proof
1745     intro_TAC ∀A O B A' O' B' G G', H1, H2;
1746     ¬Collinear A O B ∧ ¬Collinear A' O' B'     [AOBncol] by fol H1 IN_InteriorAngle;
1747     ¬(A = O) ∧ ¬(A = B) ∧ ¬(O = B) ∧ ¬(A' = O') ∧ ¬(A' = B') ∧ ¬(O' = B') ∧ ¬(G = O)     [Distinct] by fol - NonCollinearImpliesDistinct H1 InteriorEZHelp;
1748     consider a b such that
1749     Line a ∧ O ∈ a ∧ A ∈ a  ∧
1750     Line b ∧ O ∈ b ∧ B ∈ b     [a_line] by fol Distinct I1;
1751     consider g such that
1752     Line g ∧ O ∈ g ∧ G ∈ g     [g_line] by fol  Distinct I1;
1753     G ∉ a ∧ G,B same_side a     [H1'] by fol a_line H1 InteriorUse;
1754     ¬Collinear A O G ∧ ¬Collinear A' O' G'     [AOGncol] by fol H1 InteriorEZHelp IN_InteriorAngle;
1755     Angle (∡ A O B) ∧ Angle (∡ A' O' B') ∧ Angle (∡ A O G) ∧ Angle (∡ A' O' G')     [angles] by fol AOBncol - ANGLE;
1756     ∃! r. Ray r ∧ ∃X. ¬(O = X) ∧ r = ray O X ∧ X ∉ a ∧ X,G same_side a ∧ ∡ A O X ≡ ∡ A' O' B'     [] by simplify C4 - angles Distinct a_line H1';
1757     consider X such that
1758     X ∉ a ∧ X,G same_side a ∧ ∡ A O X ≡ ∡ A' O' B'     [Xexists] by fol -;
1759     ¬Collinear A O X     [AOXncol] by fol Distinct a_line Xexists NonCollinearRaa CollinearSymmetry;
1760     ∡ A' O' B' ≡ ∡ A O X     [] by fol - AOBncol ANGLE Xexists C5Symmetric;
1761     consider Y such that
1762     Y ∈ int_angle A O X  ∧  ∡ A' O' G' ≡ ∡ A O Y     [YintAOX] by fol AOXncol - H1 OrderedCongruentAngles;
1763     ¬Collinear A O Y     [] by fol - InteriorEZHelp;
1764     ∡ A O Y  ≡ ∡ A O G     [AOGeq] by fol - angles - ANGLE YintAOX H2 C5Transitive C5Symmetric;
1765     consider x such that
1766     Line x ∧ O ∈ x ∧ X ∈ x     [x_line] by fol Distinct I1;
1767     Y ∉ a ∧ Y,X same_side a     [] by fol a_line - YintAOX InteriorUse;
1768     Y ∉ a ∧ Y,G same_side a     [] by fol  a_line - Xexists H1' SameSideTransitive;
1769     ray O G = ray O Y     [] by fol a_line Distinct H1' - AOGeq C4Uniqueness;
1770     G ∈ ray O Y ━ {O}     [] by fol Distinct - EndpointInRay IN_DIFF IN_SING;
1771     G ∈ int_angle A O X     [GintAOX] by fol YintAOX - WholeRayInterior;
1772     ∡ G O X ≡ ∡ G' O' B'     [GOXeq] by fol - H1 Xexists H2 AngleSubtraction;
1773     ¬Collinear G O X ∧ ¬Collinear G O B ∧ ¬Collinear G' O' B'     [GOXncol] by fol GintAOX H1 InteriorAngleSymmetry InteriorEZHelp CollinearSymmetry;
1774     Angle (∡ G O X) ∧ Angle (∡ G O B) ∧ Angle (∡ G' O' B')     [] by fol - ANGLE;
1775     ∡ G O X ≡ ∡ G O B     [G'O'Xeq] by fol  angles - GOXeq C5Symmetric H2 C5Transitive;
1776     ¬(A,X same_side g) ∧ ¬(A,B same_side g)     [Ansim_aXB] by fol g_line GintAOX H1 InteriorOpposite;
1777     A ∉ g ∧ B ∉ g ∧ X ∉ g     [notABXg] by fol g_line AOGncol GOXncol Distinct I1 Collinear_DEF ∉;
1778     X,B same_side g     [] by fol g_line - Ansim_aXB AtMost2Sides;
1779     ray O X = ray O B     [] by fol g_line Distinct notABXg - G'O'Xeq C4Uniqueness;
1780     fol - Xexists Angle_DEF;
1781   qed;
1782 `;;
1783
1784 let AngleOrderingUse = theorem `;
1785   ∀A O B α.  Angle α  ∧  ¬Collinear A O B  ⇒  α <_ang ∡ A O B
1786     ⇒  ∃G. G ∈ int_angle A O B ∧ α ≡ ∡ A O G
1787
1788   proof
1789     intro_TAC ∀A O B α, H1, H3;
1790     consider A' O' B' G' such that
1791     ¬Collinear A' O' B'  ∧  ∡ A O B = ∡ A' O' B'  ∧  G' ∈ int_angle A' O' B'  ∧  α ≡ ∡ A' O' G'     [H3'] by fol H3 AngleOrdering_DEF;
1792     Angle (∡ A O B) ∧ Angle (∡ A' O' B') ∧ Angle (∡ A' O' G')     [angles] by fol H1 - ANGLE InteriorEZHelp;
1793     ∡ A' O' B' ≡ ∡ A O B     [] by fol - H3' C5Reflexive;
1794     consider G such that
1795     G ∈ int_angle A O B  ∧  ∡ A' O' G' ≡ ∡ A O G     [GintAOB] by fol H1 H3' -  OrderedCongruentAngles;
1796     α ≡ ∡ A O G     [] by fol H1 angles - InteriorEZHelp ANGLE H3' GintAOB C5Transitive;
1797     fol - GintAOB;
1798   qed;
1799 `;;
1800
1801 let AngleTrichotomy1 = theorem `;
1802   ∀α β. α <_ang β  ⇒  ¬(α ≡ β)
1803
1804   proof
1805     intro_TAC ∀α β, H1;
1806     assume α ≡ β     [Con] by fol;
1807     consider A O B G such that
1808     Angle α ∧ ¬Collinear A O B ∧ β = ∡ A O B ∧ G ∈ int_angle A O B ∧ α ≡ ∡ A O G     [H1'] by fol H1 AngleOrdering_DEF;
1809     ¬(A = O) ∧ ¬(O = B) ∧ ¬Collinear A O G     [Distinct] by fol H1' NonCollinearImpliesDistinct InteriorEZHelp;
1810     consider a such that
1811     Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by fol Distinct I1;
1812     consider b such that
1813     Line b ∧ O ∈ b ∧ B ∈ b     [b_line] by fol Distinct I1;
1814     B ∉ a     [notBa] by fol a_line H1' Collinear_DEF ∉;
1815     G ∉ a ∧ G ∉ b ∧ G,B same_side a     [GintAOB] by fol a_line b_line H1' InteriorUse;
1816     ∡ A O G ≡ α     [] by fol H1' Distinct ANGLE C5Symmetric;
1817     ∡ A O G ≡ ∡ A O B     [] by fol H1' Distinct ANGLE - Con C5Transitive;
1818     ray O B = ray O G     [] by fol a_line Distinct notBa GintAOB - C4Uniqueness;
1819     G ∈ b     [] by fol Distinct - EndpointInRay b_line RayLine SUBSET;
1820     fol - GintAOB ∉;
1821   qed;
1822 `;;
1823
1824 let AngleTrichotomy2 = theorem `;
1825   ∀α β γ.  α <_ang β  ∧  Angle γ  ∧  β ≡ γ  ⇒  α <_ang γ
1826
1827   proof
1828     intro_TAC ∀α β γ, H1 H2 H3;
1829     consider A O B G such that
1830     Angle α ∧ ¬Collinear A O B ∧ β = ∡ A O B ∧ G ∈ int_angle A O B ∧ α ≡ ∡ A O G     [H1'] by fol H1 AngleOrdering_DEF;
1831     consider A' O' B' such that
1832     γ = ∡ A' O' B' ∧ ¬Collinear A' O' B'     [γA'O'B'] by fol H2 ANGLE;
1833     consider G' such that
1834     G' ∈ int_angle A' O' B' ∧ ∡ A O G ≡ ∡ A' O' G'     [G'intA'O'B'] by fol γA'O'B' H1' H3  OrderedCongruentAngles;
1835     ¬Collinear A O G ∧ ¬Collinear A' O' G'     [ncol] by fol H1' - InteriorEZHelp;
1836     α ≡ ∡ A' O' G'     [] by fol H1' ANGLE - G'intA'O'B' C5Transitive;
1837     fol H1' - ncol γA'O'B' G'intA'O'B' - AngleOrdering_DEF;
1838   qed;
1839 `;;
1840
1841 let AngleOrderTransitivity = theorem `;
1842   ∀α β γ. α <_ang β  ∧  β <_ang γ  ⇒  α <_ang γ
1843
1844   proof
1845     intro_TAC ∀α β γ, H1 H2;
1846     consider A O B G such that
1847     Angle β ∧ ¬Collinear A O B ∧ γ = ∡ A O B ∧ G ∈ int_angle A O B ∧ β ≡ ∡ A O G     [H2'] by fol H2 AngleOrdering_DEF;
1848     ¬Collinear A O G     [AOGncol] by fol H2'  InteriorEZHelp;
1849     Angle α ∧ Angle (∡ A O G)  ∧ Angle γ     [angles] by fol H1 AngleOrdering_DEF H2' - ANGLE;
1850     α <_ang ∡ A O G     [] by fol H1 H2' - AngleTrichotomy2;
1851     consider F such that
1852     F ∈ int_angle A O G ∧ α ≡ ∡ A O F     [FintAOG] by fol angles AOGncol - AngleOrderingUse;
1853     F ∈ int_angle A O B     [] by fol H2' - InteriorTransitivity;
1854     fol angles H2' - FintAOG AngleOrdering_DEF;
1855   qed;
1856 `;;
1857
1858 let AngleTrichotomy = theorem `;
1859   ∀α β.  Angle α ∧ Angle β
1860    ⇒  (α ≡ β  ∨  α <_ang β  ∨  β <_ang α)  ∧
1861        ¬(α ≡ β  ∧  α <_ang β)  ∧
1862        ¬(α ≡ β  ∧  β <_ang α)  ∧
1863        ¬(α <_ang β  ∧  β <_ang α)
1864
1865   proof
1866     intro_TAC ∀α β, H1;
1867     ¬(α ≡ β  ∧  α <_ang β)     [Not12] by fol AngleTrichotomy1;
1868     ¬(α ≡ β  ∧  β <_ang α)     [Not13] by fol H1 C5Symmetric AngleTrichotomy1;
1869     ¬(α <_ang β  ∧  β <_ang α)     [Not23] by fol H1 AngleOrderTransitivity AngleTrichotomy1 C5Reflexive;
1870     consider P O A such that
1871     α = ∡ P O A ∧ ¬Collinear P O A     [POA] by fol H1 ANGLE;
1872     ¬(P = O) ∧ ¬(O = A)      [Distinct] by fol - NonCollinearImpliesDistinct;
1873     consider a such that
1874     Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by fol - I1;
1875     P ∉ a     [notPa] by fol - Distinct I1 POA Collinear_DEF ∉;
1876     ∃! r. Ray r ∧ ∃Q. ¬(O = Q) ∧ r = ray O Q ∧ Q ∉ a ∧ Q,P same_side a ∧ ∡ A O Q ≡ β     [] by simplify H1 Distinct a_line C4 -;
1877     consider Q such that
1878     ¬(O = Q) ∧ Q ∉ a ∧ Q,P same_side a ∧ ∡ A O Q ≡ β     [Qexists] by fol -;
1879     O ∉ Open (Q, P)     [notQOP] by fol a_line Qexists SameSide_DEF ∉;
1880     ¬Collinear A O P     [AOPncol] by fol POA CollinearSymmetry;
1881     ¬Collinear A O Q     [AOQncol] by fol a_line Distinct I1 Collinear_DEF Qexists ∉;
1882     Angle (∡ A O P) ∧ Angle (∡ A O Q)     [] by fol AOPncol - ANGLE;
1883     α ≡ ∡ A O P  ∧  β ≡ ∡ A O Q  ∧  ∡ A O P ≡ α     [flip] by fol H1 - POA AngleSymmetry C5Reflexive Qexists C5Symmetric;
1884     case_split QOPcol | QOPcolncol     by fol -;
1885     suppose Collinear Q O P;
1886       Collinear O P Q     [] by fol - CollinearSymmetry;
1887       Q ∈ ray O P ━ {O}     [] by fol Distinct - notQOP IN_Ray Qexists IN_DIFF IN_SING;
1888       ray O Q = ray O P     [] by fol Distinct - RayWellDefined;
1889       ∡ P O A = ∡ A O Q     [] by fol - Angle_DEF AngleSymmetry;
1890       fol - POA Qexists Not12 Not13 Not23;
1891     end;
1892     suppose ¬Collinear Q O P;
1893       P ∈ int_angle Q O A ∨ Q ∈ int_angle P O A     [] by fol Distinct a_line Qexists notPa - AngleOrdering;
1894       P ∈ int_angle A O Q ∨ Q ∈ int_angle A O P     [] by fol - InteriorAngleSymmetry;
1895       α <_ang ∡ A O Q  ∨  β <_ang ∡ A O P     [] by fol H1 AOQncol AOPncol - flip AngleOrdering_DEF;
1896       α <_ang β  ∨  β <_ang α     [] by fol H1 - Qexists flip AngleTrichotomy2;
1897       fol - Not12 Not13 Not23;
1898     end;
1899   qed;
1900 `;;
1901
1902 let SupplementExists = theorem `;
1903   ∀α. Angle α  ⇒  ∃α'. α suppl α'
1904
1905   proof
1906     intro_TAC ∀α, H1;
1907     consider A O B such that
1908     α = ∡ A O B ∧ ¬Collinear A O B ∧ ¬(A = O)     [def_α] by fol H1 ANGLE NonCollinearImpliesDistinct;
1909     consider A' such that
1910     O ∈ Open (A, A')     [AOA'] by fol - B2';
1911     ∡ A O B  suppl  ∡ A' O B     [AOBsup] by fol def_α - SupplementaryAngles_DEF AngleSymmetry;
1912     fol - def_α;
1913   qed;
1914 `;;
1915
1916 let SupplementImpliesAngle = theorem `;
1917   ∀α β.  α suppl β  ⇒  Angle α ∧ Angle β
1918
1919   proof
1920     intro_TAC ∀α β, H1;
1921     consider A O B A' such that
1922     ¬Collinear A O B  ∧  O ∈ Open (A, A')  ∧  α = ∡ A O B  ∧  β = ∡ B O A'     [H1'] by fol H1 SupplementaryAngles_DEF;
1923     ¬(O = A') ∧ Collinear A O A'     [Distinct] by fol - NonCollinearImpliesDistinct B1';
1924     ¬Collinear B O A'     [] by fol H1' CollinearSymmetry - NoncollinearityExtendsToLine;
1925     fol H1' - ANGLE;
1926   qed;
1927 `;;
1928
1929 let RightImpliesAngle = theorem `;
1930   ∀α. Right α  ⇒  Angle α
1931   by fol RightAngle_DEF SupplementImpliesAngle`;;
1932
1933 let SupplementSymmetry = theorem `;
1934   ∀α β. α suppl β  ⇒  β suppl α
1935
1936   proof
1937     intro_TAC ∀α β, H1;
1938   consider A O B A' such that
1939   ¬Collinear A O B  ∧  O ∈ Open (A, A')  ∧  α = ∡ A O B  ∧  β = ∡ B O A'     [H1'] by fol H1 SupplementaryAngles_DEF;
1940   ¬(O = A') ∧ Collinear A O A'     [] by fol - NonCollinearImpliesDistinct B1';
1941   ¬Collinear A' O B     [A'OBncol] by fol H1' CollinearSymmetry - NoncollinearityExtendsToLine;
1942   O ∈ Open (A', A)  ∧  β = ∡ A' O B  ∧  α = ∡ B O A     [] by fol H1' B1'  AngleSymmetry;
1943   fol A'OBncol - SupplementaryAngles_DEF;
1944   qed;
1945 `;;
1946
1947 let SupplementsCongAnglesCong = theorem `;
1948   ∀α β α' β'.  α suppl α'  ∧  β suppl β'  ⇒  α ≡ β
1949     ⇒  α' ≡ β'
1950
1951   proof
1952     intro_TAC ∀α β α' β', H1, H2;
1953     consider A O B A' such that
1954     ¬Collinear A O B  ∧  O ∈ Open (A, A')  ∧  α = ∡ A O B  ∧  α' = ∡ B O A'     [def_α] by fol H1 SupplementaryAngles_DEF;
1955     ¬(A = O) ∧ ¬(O = B) ∧ ¬(A = A') ∧ ¬(O = A') ∧ Collinear A O A'     [Distinctα] by fol - NonCollinearImpliesDistinct B1';
1956     ¬Collinear B A A' ∧ ¬Collinear O A' B     [BAA'ncol] by fol def_α CollinearSymmetry - NoncollinearityExtendsToLine;
1957     Segment (seg O A) ∧ Segment (seg O B) ∧ Segment (seg O A')     [Osegments] by fol Distinctα SEGMENT;
1958     consider C P D C' such that
1959     ¬Collinear C P D  ∧  P ∈ Open (C, C')  ∧  β = ∡ C P D  ∧  β' = ∡ D P C'     [def_β] by fol H1 SupplementaryAngles_DEF;
1960     ¬(C = P) ∧ ¬(P = D) ∧ ¬(P = C')     [Distinctβ] by fol def_β NonCollinearImpliesDistinct B1';
1961     consider X such that
1962     X ∈ ray P C ━ {P}  ∧  seg P X ≡ seg O A     [defX] by fol Osegments Distinctβ C1;
1963     consider Y such that
1964     Y ∈ ray P D ━ {P}  ∧  seg P Y ≡ seg O B  ∧  ¬(Y = P)     [defY] by fol Osegments Distinctβ C1 IN_DIFF IN_SING;
1965     consider X' such that
1966     X' ∈ ray P C' ━ {P}  ∧  seg P X' ≡ seg O A'     [defX'] by fol Osegments Distinctβ C1;
1967     P ∈ Open (X', C)  ∧  P ∈ Open (X, X')       [XPX'] by fol def_β - OppositeRaysIntersect1pointHelp defX;
1968     ¬(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 fol defX defX' IN_DIFF IN_SING - B1' def_α IntervalRay;
1969      Collinear P D Y ∧ Collinear P C X     [] by fol defY defX IN_DIFF IN_SING IN_Ray;
1970     ¬Collinear C P Y ∧ ¬Collinear X P Y     [XPYncol] by fol def_β - defY NoncollinearityExtendsToLine CollinearSymmetry XPX'line;
1971     ¬Collinear Y X X' ∧ ¬Collinear P X' Y     [YXX'ncol] by fol - CollinearSymmetry XPX' XPX'line NoncollinearityExtendsToLine;
1972     ray P X = ray P C  ∧  ray P Y = ray P D  ∧  ray P X' = ray P C'     [equalPrays] by fol Distinctβ defX defY defX' RayWellDefined;
1973     β = ∡ X P Y  ∧  β' = ∡ Y P X'  ∧  ∡ A O B ≡ ∡ X P Y     [AOBeqXPY] by fol def_β - Angle_DEF H2 def_α;
1974    seg O A ≡ seg P X  ∧  seg O B ≡ seg P Y  ∧  seg A' O ≡ seg X' P     [OAeq] by fol Osegments XPX'line SEGMENT defX defY defX' C2Symmetric SegmentSymmetry;
1975     seg A A' ≡ seg X X'     [AA'eq] by fol def_α XPX'line XPX' - SegmentSymmetry C3;
1976     A,O,B ≅ X,P,Y     [] by fol def_α XPYncol OAeq AOBeqXPY SAS;
1977     seg A B ≡ seg X Y  ∧  ∡ B A O ≡ ∡ Y X P     [AOB≅] by fol - TriangleCong_DEF AngleSymmetry;
1978     ray A O = ray A A'  ∧  ray X P = ray X  X'  ∧  ∡ B A A' ≡ ∡ Y X X'     [] by fol def_α XPX' IntervalRay - Angle_DEF;
1979     B,A,A' ≅ Y,X,X'     [] by fol BAA'ncol YXX'ncol AOB≅ - AA'eq - SAS;
1980     seg A' B ≡ seg X' Y  ∧  ∡ A A' B ≡ ∡ X X' Y     [] by fol - TriangleCong_DEF SegmentSymmetry;
1981     O,A',B ≅ P,X',Y     [] by fol BAA'ncol YXX'ncol OAeq - XPX'line Angle_DEF SAS;
1982     ∡ B O A' ≡ ∡ Y P X'     [] by fol - TriangleCong_DEF;
1983     fol - equalPrays def_β Angle_DEF def_α;
1984   qed;
1985 `;;
1986
1987 let SupplementUnique = theorem `;
1988   ∀α β β'.  α suppl β  ∧   α suppl β'  ⇒  β ≡ β'
1989   by fol SupplementaryAngles_DEF ANGLE C5Reflexive SupplementsCongAnglesCong`;;
1990
1991 let CongRightImpliesRight = theorem `;
1992   ∀α β. Angle α  ∧  Right β  ⇒  α ≡ β  ⇒  Right α
1993
1994   proof
1995     intro_TAC ∀α β, H1, H2;
1996     consider α' β' such that
1997     α suppl α'  ∧  β suppl β'  ∧  β ≡ β'     [suppl] by fol H1 SupplementExists H1 RightAngle_DEF;
1998     α' ≡ β'     [α'eqβ'] by fol suppl H2 SupplementsCongAnglesCong;
1999     Angle β ∧ Angle α' ∧ Angle β'     [] by fol suppl SupplementImpliesAngle;
2000     α ≡ α'     [] by fol     H1 - H2 suppl α'eqβ' C5Symmetric C5Transitive;
2001     fol suppl - RightAngle_DEF;
2002   qed;
2003 `;;
2004
2005 let RightAnglesCongruentHelp = theorem `;
2006   ∀A O B A' P a.  ¬Collinear A O B  ∧  O ∈ Open (A, A')  ⇒
2007     Right (∡ A O B)  ∧  Right (∡ A O P)
2008     ⇒  P ∉ int_angle A O B
2009
2010   proof
2011     intro_TAC ∀A O B A' P a, H1, H2;
2012     assume ¬(P ∉ int_angle A O B)     [Con] by fol;
2013     P ∈ int_angle A O B     [PintAOB] by fol - ∉;
2014     B ∈ int_angle P O A'  ∧  B ∈ int_angle A' O P     [BintA'OP] by fol H1 - InteriorReflectionInterior InteriorAngleSymmetry ;
2015     ¬Collinear A O P ∧ ¬Collinear P O A'     [AOPncol] by fol PintAOB InteriorEZHelp - IN_InteriorAngle;
2016     ∡ A O B suppl ∡ B O A'  ∧  ∡ A O P suppl ∡ P O A'     [AOBsup] by fol H1 - SupplementaryAngles_DEF;
2017     consider α' β' such that
2018     ∡ A O B suppl α'  ∧  ∡ A O B ≡ α'  ∧  ∡ A O P suppl β'  ∧  ∡ A O P ≡ β'     [supplα'] by fol H2 RightAngle_DEF;
2019     α' ≡ ∡ B O A'  ∧  β' ≡ ∡ P O A'     [α'eqA'OB] by fol - AOBsup SupplementUnique;
2020     Angle (∡ A O B) ∧ Angle α' ∧ Angle (∡ B O A') ∧ Angle (∡ A O P) ∧ Angle β' ∧ Angle (∡ P O A')     [angles] by fol AOBsup supplα' SupplementImpliesAngle AngleSymmetry;
2021     ∡ A O B ≡ ∡ B O A'  ∧  ∡ A O P ≡ ∡ P O A'     [H2'] by fol - supplα' α'eqA'OB C5Transitive;
2022     ∡ A O P ≡ ∡ A O P  ∧  ∡ B O A' ≡ ∡ B O A'     [refl] by fol angles C5Reflexive;
2023     ∡ A O P <_ang ∡ A O B  ∧  ∡ B O A' <_ang ∡ P O A'     [BOA'lessPOA'] by fol angles H1 PintAOB - AngleOrdering_DEF AOPncol CollinearSymmetry BintA'OP AngleSymmetry;
2024     ∡ A O P <_ang ∡ B O A'     [] by fol - angles H2' AngleTrichotomy2;
2025     ∡ A O P <_ang ∡ P O A'     [] by fol - BOA'lessPOA' AngleOrderTransitivity;
2026     fol - H2' AngleTrichotomy1;
2027   qed;
2028 `;;
2029
2030 let RightAnglesCongruent = theorem `;
2031   ∀α β. Right α ∧ Right β  ⇒  α ≡ β
2032
2033   proof
2034     intro_TAC ∀α β, H1;
2035     consider α' such that
2036     α suppl α'  ∧  α ≡ α'     [αright] by fol H1 RightAngle_DEF;
2037     consider A O B A' such that
2038     ¬Collinear A O B  ∧  O ∈ Open (A, A')  ∧  α = ∡ A O B  ∧  α' = ∡ B O A'     [def_α] by fol - SupplementaryAngles_DEF;
2039     ¬(A = O) ∧ ¬(O = B)     [Distinct] by fol def_α NonCollinearImpliesDistinct B1';
2040     consider a such that
2041     Line a ∧ O ∈ a ∧ A ∈ a     [a_line] by fol Distinct I1;
2042     B ∉ a     [notBa] by fol - def_α Collinear_DEF ∉;
2043     Angle β     [] by fol H1 RightImpliesAngle;
2044     ∃! r. Ray r ∧ ∃P. ¬(O = P) ∧ r = ray O P ∧ P ∉ a ∧ P,B same_side a ∧ ∡ A O P ≡ β     [] by simplify C4 - Distinct a_line notBa;
2045     consider P such that
2046     ¬(O = P) ∧ P ∉ a ∧ P,B same_side a ∧ ∡ A O P ≡ β     [defP] by fol -;
2047     O ∉ Open (P, B)     [notPOB] by fol a_line - SameSide_DEF ∉;
2048     ¬Collinear A O P     [AOPncol] by fol a_line Distinct defP NonCollinearRaa CollinearSymmetry;
2049     Right (∡ A O P)     [AOPright] by fol - ANGLE H1 defP CongRightImpliesRight;
2050     P ∉ int_angle A O B  ∧  B ∉ int_angle A O P     [] by fol def_α H1 - AOPncol AOPright RightAnglesCongruentHelp;
2051     Collinear P O B     [] by fol Distinct a_line defP notBa - AngleOrdering InteriorAngleSymmetry ∉;
2052     P ∈ ray O B ━ {O}     [] by fol Distinct - CollinearSymmetry notPOB IN_Ray defP IN_DIFF IN_SING;
2053     ray O P = ray O B  ∧  ∡ A O P = ∡ A O B     [] by fol Distinct - RayWellDefined Angle_DEF;
2054     fol - defP def_α;
2055   qed;
2056 `;;
2057
2058 let OppositeRightAnglesLinear = theorem `;
2059   ∀A B O H h.  ¬Collinear A O H ∧ ¬Collinear H O B  ⇒
2060     Right (∡ A O H) ∧ Right (∡ H O B)  ⇒
2061     Line h ∧ O ∈ h ∧ H ∈ h  ∧  ¬(A,B same_side h)
2062     ⇒  O ∈ Open (A, B)
2063
2064   proof
2065     intro_TAC ∀A B O H h, H0, H1, H2;
2066     ¬(A = O) ∧ ¬(O = H) ∧ ¬(O = B)     [Distinct] by fol  H0 NonCollinearImpliesDistinct;
2067     A ∉ h ∧ B ∉ h     [notABh] by fol H0 H2 Collinear_DEF ∉;
2068     consider E such that
2069     O ∈ Open (A, E) ∧ ¬(E = O)     [AOE] by fol Distinct B2' B1';
2070     ∡ A O H  suppl  ∡ H O E     [AOHsupplHOE] by fol H0 - SupplementaryAngles_DEF;
2071     E ∉ h     [notEh] by fol H2 ∉ AOE BetweenLinear notABh;
2072     ¬(A,E same_side  h)     [] by fol H2 AOE SameSide_DEF;
2073     B,E same_side  h     [Bsim_hE] by fol H2 notABh notEh - H2 AtMost2Sides;
2074     consider α' such that
2075     ∡ A O H  suppl  α'  ∧  ∡ A O H ≡ α'     [AOHsupplα'] by fol H1 RightAngle_DEF;
2076     Angle (∡ H O B) ∧ Angle (∡ A O H) ∧ Angle α' ∧ Angle (∡ H O E)     [angα'] by fol H1 RightImpliesAngle - AOHsupplHOE SupplementImpliesAngle;
2077     ∡ H O B ≡ ∡ A O H  ∧  α' ≡ ∡ H O E     [] by fol H1 RightAnglesCongruent AOHsupplα' AOHsupplHOE SupplementUnique;
2078     ∡ H O B ≡ ∡ H O E     [] by fol angα' - AOHsupplα' C5Transitive;
2079     ray O B = ray O E     [] by fol H2 Distinct notABh notEh Bsim_hE - C4Uniqueness;
2080     B ∈ ray O E ━ {O}     [] by fol Distinct EndpointInRay - IN_DIFF IN_SING;
2081     fol AOE - OppositeRaysIntersect1pointHelp B1';
2082   qed;
2083 `;;
2084
2085 let RightImpliesSupplRight = theorem `;
2086   ∀A O B A'.  ¬Collinear A O B  ∧  O ∈ Open (A, A')  ∧  Right (∡ A O B)
2087     ⇒  Right (∡ B O A')
2088
2089   proof
2090     intro_TAC ∀A O B A', H1 H2 H3;
2091     ∡ A O B suppl ∡ B O A'  ∧  Angle (∡ A O B)  ∧  Angle (∡ B O A')     [AOBsuppl] by fol H1 H2 SupplementaryAngles_DEF SupplementImpliesAngle;
2092     consider β such that
2093     ∡ A O B suppl β ∧ ∡ A O B ≡ β     [βsuppl] by fol H3 RightAngle_DEF;
2094     Angle β  ∧  β ≡ ∡ A O B     [angβ] by fol - SupplementImpliesAngle C5Symmetric;
2095     ∡ B O A' ≡ β     [] by fol AOBsuppl βsuppl SupplementUnique;
2096     ∡ B O A' ≡ ∡ A O B     [] by fol AOBsuppl angβ - βsuppl C5Transitive;
2097     fol AOBsuppl H3 - CongRightImpliesRight;
2098   qed;
2099 `;;
2100
2101 let IsoscelesCongBaseAngles = theorem `;
2102   ∀A B C.  ¬Collinear A B C  ∧  seg B A ≡ seg B C  ⇒   ∡ C A B  ≡ ∡ A C B
2103
2104   proof
2105     intro_TAC ∀A B C, H1 H2;
2106     ¬(A = B) ∧ ¬(B = C) ∧ ¬Collinear C B A     [CBAncol] by fol H1 NonCollinearImpliesDistinct CollinearSymmetry;
2107     seg B C ≡ seg B A  ∧  ∡ A B C ≡ ∡ C B A     [] by fol - SEGMENT H2 C2Symmetric H1 ANGLE AngleSymmetry C5Reflexive;
2108     fol H1 CBAncol H2 - SAS TriangleCong_DEF;
2109   qed;
2110 `;;
2111
2112 let C4withC1 = theorem `;
2113   ∀α l O A Y P Q.  Angle α ∧ ¬(O = A) ∧ ¬(P = Q)  ⇒
2114     Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l  ⇒
2115     ∃N. ¬(O = N) ∧ N ∉ l ∧ N,Y same_side l ∧ seg O N ≡ seg P Q ∧ ∡ A O N ≡ α
2116
2117   proof
2118     intro_TAC ∀α l O A Y P Q, H1, l_line;
2119     ∃! r. Ray r ∧ ∃B. ¬(O = B) ∧ r = ray O B ∧ B ∉ l ∧ B,Y same_side l ∧ ∡ A O B ≡ α     [] by simplify C4 H1 l_line;
2120     consider B such that
2121     ¬(O = B) ∧ B ∉ l ∧ B,Y same_side l ∧ ∡ A O B ≡ α     [Bexists] by fol -;
2122     consider N such that
2123     N ∈ ray O B ━ {O}  ∧  seg O N ≡ seg P Q     [Nexists] by fol H1 - SEGMENT C1;
2124     N ∉ l ∧ N,B same_side l     [notNl] by fol l_line Bexists Nexists RaySameSide;
2125     N,Y same_side l     [Nsim_lY] by fol l_line - Bexists SameSideTransitive;
2126     ray O N = ray O B     [] by fol Bexists Nexists RayWellDefined;
2127     ∡ A O N ≡ α     [] by fol - Bexists Angle_DEF;
2128     fol Nexists IN_DIFF IN_SING notNl Nsim_lY Nexists -;
2129   qed;
2130 `;;
2131
2132 let C4OppositeSide = theorem `;
2133   ∀α l O A Z P Q.  Angle α ∧ ¬(O = A) ∧ ¬(P = Q)  ⇒
2134     Line l ∧ O ∈ l ∧ A ∈ l ∧ Z ∉ l
2135     ⇒  ∃N. ¬(O = N) ∧ N ∉ l ∧ ¬(Z,N same_side l) ∧
2136     seg O N ≡ seg P Q ∧ ∡ A O N ≡ α
2137
2138   proof
2139     intro_TAC ∀α l O A Z P Q, H1, l_line;
2140     ¬(Z = O)     [] by fol l_line ∉;
2141     consider Y such that
2142     O ∈ Open (Z, Y)     [ZOY] by fol - B2';
2143     ¬(O = Y) ∧ Collinear O Z Y     [notOY] by fol - B1' CollinearSymmetry;
2144     Y ∉ l     [notYl] by fol notOY l_line NonCollinearRaa ∉;
2145     consider N such that
2146     ¬(O = N) ∧ N ∉ l  ∧  N,Y same_side l  ∧ seg O N ≡ seg P Q  ∧  ∡ A O N ≡ α     [Nexists] by simplify C4withC1 H1 l_line -;
2147     ¬(Z,Y same_side l)     [] by fol l_line ZOY SameSide_DEF;
2148     ¬(Z,N same_side l)     [] by fol l_line Nexists notYl - SameSideTransitive;
2149     fol - Nexists;
2150   qed;
2151 `;;
2152
2153 let SSS = theorem `;
2154   ∀A B C A' B' C'.  ¬Collinear A B C ∧ ¬Collinear A' B' C'  ⇒
2155     seg A B ≡ seg A' B'  ∧  seg A C ≡ seg A' C'  ∧  seg B C ≡ seg B' C'
2156     ⇒  A,B,C ≅ A',B',C'
2157
2158   proof
2159     intro_TAC ∀A B C A' B' C', H1, H2;
2160     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬(A' = B') ∧ ¬(B' = C')     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2161     consider h such that
2162     Line h ∧ A ∈ h ∧ C ∈ h     [h_line] by fol Distinct I1;
2163     B ∉ h     [notBh] by fol h_line H1 ∉ Collinear_DEF;
2164     Segment (seg A B) ∧ Segment (seg C B) ∧ Segment (seg A' B') ∧ Segment (seg C' B')     [segments] by fol Distinct - SEGMENT;
2165     Angle (∡ C' A' B')     [] by fol H1 CollinearSymmetry ANGLE;
2166     consider N such that
2167     ¬(A = N) ∧ N ∉ h ∧ ¬(B,N same_side h) ∧ seg A N ≡ seg A' B'  ∧  ∡ C A N ≡ ∡ C' A' B'     [Nexists] by simplify C4OppositeSide - Distinct h_line notBh;
2168     ¬(C = N)     [] by fol h_line Nexists ∉;
2169     Segment (seg A N) ∧ Segment (seg C N)     [segN] by fol Nexists - SEGMENT;
2170     ¬Collinear A N C     [ANCncol] by fol Distinct h_line Nexists NonCollinearRaa;
2171     Angle (∡ A B C) ∧ Angle (∡ A' B' C') ∧ Angle (∡ A N C)     [angles] by fol H1 - ANGLE;
2172     seg A B ≡ seg A N     [ABeqAN] by fol segments segN Nexists H2 C2Symmetric C2Transitive;
2173     C,A,N ≅ C',A',B'     [] by fol ANCncol H1 CollinearSymmetry H2 Nexists SAS;
2174     ∡ A N C ≡ ∡ A' B' C'  ∧  seg C N ≡ seg C' B'     [ANCeq] by fol - TriangleCong_DEF;
2175     seg C B ≡ seg C N     [CBeqCN] by fol segments segN - H2 SegmentSymmetry C2Symmetric C2Transitive;
2176     consider G such that
2177     G ∈ h ∧ G ∈ Open (B, N)     [BGN] by fol Nexists h_line SameSide_DEF;
2178     ¬(B = N)     [notBN] by fol - B1';
2179     ray B G = ray B N  ∧  ray N G = ray N B     [Grays] by fol BGN B1' IntervalRay;
2180     consider v such that
2181     Line v ∧ B ∈ v ∧ N ∈ v     [v_line] by fol notBN I1;
2182     G ∈ v ∧ ¬(h = v)     [] by fol v_line BGN BetweenLinear notBh ∉;
2183     h ∩ v = {G}     [hvG] by fol h_line v_line - BGN I1Uniqueness;
2184     ¬(G = A)  ⇒  ∡ A B G ≡ ∡ A N G     [ABGeqANG]
2185     proof
2186       intro_TAC notGA;
2187       A ∉ v     [] by fol hvG h_line - EquivIntersectionHelp IN_DIFF IN_SING;
2188       ¬Collinear B A N     [] by fol v_line notBN I1 Collinear_DEF - ∉;
2189       ∡ N B A ≡ ∡ B N A     [] by fol - ABeqAN IsoscelesCongBaseAngles;
2190       ∡ G B A ≡ ∡ G N A     [] by fol - Grays Angle_DEF notGA;
2191       fol - AngleSymmetry;
2192     qed;
2193     ¬(G = C)  ⇒  ∡ G B C ≡ ∡ G N C     [GBCeqGNC]
2194     proof
2195       intro_TAC notGC;
2196       C ∉ v     [] by fol hvG h_line - EquivIntersectionHelp IN_DIFF IN_SING;
2197       ¬Collinear B C N     [] by fol v_line notBN I1 Collinear_DEF - ∉;
2198       ∡ N B C ≡ ∡ B N C     [] by fol - CBeqCN IsoscelesCongBaseAngles AngleSymmetry;
2199       fol - Grays Angle_DEF;
2200     qed;
2201     ∡ A B C ≡ ∡ A N C     []
2202     proof
2203       assume ¬(G = A) ∧ ¬(G = C) [AGCdistinct] by fol Distinct GBCeqGNC ABGeqANG;
2204       ∡ A B G ≡ ∡ A N G  ∧  ∡ G B C ≡ ∡ G N C     [Gequivs] by fol - ABGeqANG GBCeqGNC;
2205       ¬Collinear G B C ∧ ¬Collinear G N C ∧ ¬Collinear G B A ∧ ¬Collinear G N A     [Gncols] by fol AGCdistinct h_line BGN notBh Nexists NonCollinearRaa;
2206       Collinear A G C     [] by fol h_line BGN Collinear_DEF;
2207       G ∈ Open (A, C) ∨ C ∈ Open (G, A) ∨ A ∈ Open (C, G)     [] by fol Distinct AGCdistinct - B3';
2208       case_split AGC | GAC | CAG     by fol -;
2209       suppose G ∈ Open (A, C);
2210         G ∈ int_angle A B C  ∧  G ∈ int_angle A N C     [] by fol H1 ANCncol - ConverseCrossbar;
2211         fol - Gequivs AngleAddition;
2212       end;
2213       suppose C ∈ Open (G, A);
2214         C ∈ int_angle G B A  ∧  C ∈ int_angle G N A     [] by fol Gncols - B1' ConverseCrossbar;
2215         fol - Gequivs AngleSubtraction AngleSymmetry;
2216       end;
2217       suppose A ∈ Open (C, G);
2218         A ∈ int_angle G B C  ∧  A ∈ int_angle G N C     [] by fol Gncols - B1' ConverseCrossbar;
2219         fol - Gequivs AngleSymmetry AngleSubtraction;
2220       end;
2221     qed;
2222     ∡ A B C ≡ ∡ A' B' C'     [] by fol angles - ANCeq C5Transitive;
2223     fol H1 H2 SegmentSymmetry - SAS;
2224   qed;
2225 `;;
2226
2227 let AngleBisector = theorem `;
2228   ∀A B C. ¬Collinear B A C  ⇒  ∃M. M ∈ int_angle B A C  ∧  ∡ B A M ≡ ∡ M A C
2229
2230   proof
2231     intro_TAC ∀A B C, H1;
2232     ¬(A = B) ∧ ¬(A = C)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2233     consider D such that
2234     B ∈ Open (A, D)     [ABD] by fol Distinct B2';
2235     ¬(A = D) ∧ Collinear A B D ∧ Segment (seg A D)     [ABD'] by fol - B1' SEGMENT;
2236     consider E such that
2237     E ∈ ray A C ━ {A}  ∧  seg A E ≡ seg A D  ∧  ¬(A = E)     [ErAC] by fol - Distinct C1 IN_Ray IN_DIFF IN_SING;
2238     Collinear A C E  ∧  D ∈ ray A B ━ {A}     [notAE] by fol - IN_Ray ABD IntervalRayEZ IN_DIFF IN_SING;
2239     ray A D = ray A B  ∧  ray A E =  ray A C     [equalrays] by fol Distinct notAE ErAC RayWellDefined;
2240     ¬Collinear D A E ∧ ¬Collinear E A D ∧ ¬Collinear A E D     [EADncol] by fol H1 ABD' notAE ErAC CollinearSymmetry NoncollinearityExtendsToLine;
2241     ∡ D E A ≡ ∡ E D A     [DEAeq] by fol EADncol ErAC IsoscelesCongBaseAngles;
2242     ¬Collinear E D A ∧ Angle (∡ E D A) ∧ ¬Collinear A D E ∧ ¬Collinear D E A     [angEDA] by fol EADncol CollinearSymmetry ANGLE;
2243     ¬(D = E)     [notDE] by fol EADncol NonCollinearImpliesDistinct;
2244     consider h such that
2245     Line h ∧ D ∈ h ∧ E ∈ h     [h_line] by fol - I1;
2246     A ∉ h     [notAh] by fol - Collinear_DEF EADncol ∉;
2247     consider M such that
2248     ¬(D = M)  ∧  M ∉ h  ∧  ¬(A,M same_side h)  ∧  seg D M ≡ seg D A  ∧  ∡ E D M ≡ ∡ E D A     [Mexists] by simplify C4OppositeSide angEDA notDE ABD' h_line -;
2249     ¬(A = M)     [notAM] by fol h_line - SameSideReflexive;
2250     ¬Collinear E D M ∧ ¬Collinear D E M ∧ ¬Collinear M E D     [EDMncol] by fol  notDE h_line Mexists NonCollinearRaa CollinearSymmetry;
2251     seg D E ≡ seg D E  ∧  seg M A ≡ seg M A     [MArefl] by fol notDE notAM SEGMENT C2Reflexive;
2252     E,D,M ≅ E,D,A     [] by fol EDMncol angEDA - Mexists SAS;
2253     seg M E ≡ seg A E ∧ ∡ M E D ≡ ∡ A E D ∧ ∡ D E M ≡ ∡ D E A     [MED≅] by fol - TriangleCong_DEF SegmentSymmetry AngleSymmetry;
2254     ∡ E D A ≡ ∡ D E A  ∧  ∡ E D A ≡ ∡ E D M  ∧  ∡ D E A ≡ ∡ D E M     [EDAeqEDM] by fol EDMncol ANGLE angEDA Mexists MED≅ DEAeq C5Symmetric;
2255     consider G such that
2256     G ∈ h ∧ G ∈ Open (A, M)     [AGM] by fol Mexists h_line SameSide_DEF;
2257     M ∈ ray A G ━ {A}     [MrAG] by fol - IntervalRayEZ;
2258     consider v such that
2259     Line v ∧ A ∈ v ∧ M ∈ v ∧ G ∈ v     [v_line] by fol notAM I1 AGM BetweenLinear;
2260     ¬(v = h)  ∧  v ∩ h = {G}     [vhG] by fol - notAh ∉ h_line AGM I1Uniqueness;
2261     D ∉ v     [notDv]
2262     proof
2263       assume ¬(D ∉ v)     [Con] by fol;
2264       D ∈ v  ∧  D = G     [DG] by fol h_line - ∉ vhG IN_INTER IN_SING;
2265       D ∈ Open (A, M)     [] by fol DG AGM;
2266       ∡ E D A suppl ∡ E D M     [EDAsuppl] by fol angEDA - SupplementaryAngles_DEF AngleSymmetry;
2267       Right (∡ E D A)     [] by fol EDAsuppl EDAeqEDM RightAngle_DEF;
2268       Right (∡ A E D)     [RightAED] by fol angEDA ANGLE - DEAeq CongRightImpliesRight AngleSymmetry;
2269       Right (∡ D E M)     [] by fol EDMncol ANGLE - MED≅ CongRightImpliesRight AngleSymmetry;
2270       E ∈ Open (A, M)     [] by fol EADncol EDMncol RightAED - h_line Mexists  OppositeRightAnglesLinear;
2271       E ∈ v  ∧  E = G     [] by fol v_line - BetweenLinear h_line vhG IN_INTER IN_SING;
2272       fol - DG notDE;
2273     qed;
2274     E ∉ v     [notEv]
2275     proof
2276       assume ¬(E ∉ v)     [Con] by fol;
2277       E ∈ v  ∧  E = G     [EG] by fol h_line - ∉ vhG IN_INTER IN_SING;
2278       E ∈ Open (A, M)     [] by fol - AGM;
2279       ∡ D E A suppl ∡ D E M     [DEAsuppl] by fol EADncol - SupplementaryAngles_DEF AngleSymmetry;
2280       Right (∡ D E A)     [RightDEA] by fol DEAsuppl EDAeqEDM RightAngle_DEF;
2281       Right (∡ E D A)     [RightEDA] by fol angEDA RightDEA EDAeqEDM CongRightImpliesRight;
2282       Right (∡ E D M)     [] by fol EDMncol ANGLE RightEDA Mexists CongRightImpliesRight;
2283       D ∈ Open (A, M)     [] by fol angEDA EDMncol RightEDA AngleSymmetry - h_line Mexists  OppositeRightAnglesLinear;
2284       D ∈ v ∧ D = G     [] by fol v_line - BetweenLinear h_line vhG IN_INTER IN_SING;
2285       fol - EG notDE;
2286     qed;
2287     ¬Collinear M A E ∧ ¬Collinear M A D  ∧  ¬(M = E)     [MAEncol] by fol notAM v_line notEv notDv NonCollinearRaa CollinearSymmetry NonCollinearImpliesDistinct;
2288     seg M E ≡ seg A D     [MEeqAD] by fol - ErAC ABD' SEGMENT MED≅ ErAC C2Transitive;
2289     seg A D ≡ seg M D     [] by fol SegmentSymmetry ABD' Mexists SEGMENT C2Symmetric;
2290     seg M E ≡ seg M D     [] by fol MAEncol ABD' Mexists SEGMENT MEeqAD - C2Transitive;
2291     M,A,E ≅ M,A,D     [] by fol MAEncol MArefl - ErAC SSS;
2292     ∡ M A E ≡ ∡ M A D     [MAEeq] by fol - TriangleCong_DEF;
2293     ∡ D A M ≡ ∡ M A E     [] by fol MAEncol ANGLE MAEeq C5Symmetric AngleSymmetry;
2294     ∡ B A M ≡ ∡ M A C     [BAMeqMAC] by fol - equalrays Angle_DEF;
2295     ¬(E,D same_side v)     []
2296     proof
2297       assume E,D same_side v     [Con] by fol;
2298       ray A D = ray A E     [] by fol v_line notAM notDv notEv - MAEeq C4Uniqueness;
2299       fol ABD' EndpointInRay - IN_Ray EADncol;
2300     qed;
2301     consider H such that
2302     H ∈ v ∧ H ∈ Open (E, D)     [EHD] by fol v_line - SameSide_DEF;
2303     H = G     [] by fol - h_line BetweenLinear IN_INTER vhG IN_SING;
2304     G ∈ int_angle E A D     [GintEAD] by fol EADncol  - EHD ConverseCrossbar;
2305     M ∈ int_angle E A D     [MintEAD] by fol GintEAD MrAG WholeRayInterior;
2306     B ∈ ray A D ━ {A}   ∧   C ∈ ray A E ━ {A}     [] by fol equalrays Distinct EndpointInRay IN_DIFF IN_SING;
2307     M ∈ int_angle B A C     [] by fol MintEAD - InteriorWellDefined InteriorAngleSymmetry;
2308     fol - BAMeqMAC;
2309   qed;
2310 `;;
2311
2312 let EuclidPropositionI_6 = theorem `;
2313   ∀A B C. ¬Collinear A B C  ∧  ∡ B A C ≡ ∡ B C A  ⇒  seg B A ≡ seg B C
2314
2315   proof
2316     intro_TAC ∀A B C, H1 H2;
2317     ¬(A = C)     [] by fol H1 NonCollinearImpliesDistinct;
2318     seg C A ≡ seg A C     [CAeqAC] by fol SegmentSymmetry - SEGMENT C2Reflexive;
2319     ¬Collinear B C A ∧ ¬Collinear C B A ∧ ¬Collinear B A C     [BCAncol] by fol H1 CollinearSymmetry;
2320     ∡ A C B ≡ ∡ C A B     [] by fol - ANGLE H2 C5Symmetric AngleSymmetry;
2321     C,B,A ≅ A,B,C     [] by fol H1 BCAncol CAeqAC H2 - ASA;
2322     fol - TriangleCong_DEF;
2323   qed;
2324 `;;
2325
2326 let IsoscelesExists = theorem `;
2327   ∀A B. ¬(A = B)  ⇒  ∃D. ¬Collinear A D B  ∧  seg D A ≡ seg D B
2328
2329   proof
2330     intro_TAC ∀A B, H1;
2331     consider l such that
2332     Line l ∧ A ∈ l ∧ B ∈ l     [l_line] by fol H1 I1;
2333     consider C such that
2334     C ∉ l     [notCl] by fol - ExistsPointOffLine;
2335     ¬Collinear C A B ∧ ¬Collinear C B A ∧ ¬Collinear A B C ∧ ¬Collinear A C B ∧ ¬Collinear B A C     [CABncol] by fol l_line H1 I1 Collinear_DEF - ∉;
2336     ∡ C A B ≡ ∡ C B A  ∨  ∡ C A B <_ang ∡ C B A  ∨  ∡ C B A <_ang ∡ C A B     [] by fol - ANGLE AngleTrichotomy;
2337     case_split cong | less | greater     by fol -;
2338     suppose ∡ C A B ≡ ∡ C B A;
2339       fol - CABncol EuclidPropositionI_6;
2340     end;
2341     suppose ∡ C A B <_ang ∡ C B A;
2342       ∡ C A B <_ang ∡ A B C     [] by fol - AngleSymmetry;
2343       consider E such that
2344       E ∈ int_angle A B C  ∧  ∡ C A B ≡ ∡ A B E     [Eexists] by fol CABncol ANGLE - AngleOrderingUse;
2345       ¬(B = E)     [notBE] by fol - InteriorEZHelp;
2346       consider D such that
2347       D ∈ Open (A, C)  ∧  D ∈ ray B E ━ {B}     [Dexists] by fol Eexists Crossbar_THM;
2348       D ∈ int_angle A B C     [] by fol Eexists - WholeRayInterior;
2349       ¬Collinear A D B     [ADBncol] by fol - InteriorEZHelp CollinearSymmetry;
2350       ray B D = ray B E  ∧  ray A D = ray A C     [] by fol notBE Dexists RayWellDefined IntervalRay;
2351       ∡ D A B ≡ ∡ A B D     [] by fol Eexists - Angle_DEF;
2352       fol ADBncol - AngleSymmetry EuclidPropositionI_6;
2353     end;
2354     suppose ∡ C B A <_ang ∡ C A B;
2355       ∡ C B A <_ang ∡ B A C     [] by fol - AngleSymmetry;
2356       consider E such that
2357       E ∈ int_angle B A C  ∧  ∡ C B A ≡ ∡ B A E     [Eexists] by fol CABncol ANGLE - AngleOrderingUse;
2358       ¬(A = E)     [notAE] by fol - InteriorEZHelp;
2359       consider D such that
2360       D ∈ Open (B, C) ∧ D ∈ ray A E ━ {A}     [Dexists] by fol Eexists Crossbar_THM;
2361       D ∈ int_angle B A C     [] by fol Eexists - WholeRayInterior;
2362       ¬Collinear A D B ∧ ¬Collinear D A B ∧ ¬Collinear D B A     [ADBncol] by fol - InteriorEZHelp CollinearSymmetry;
2363       ray A D = ray A E  ∧  ray B D = ray B C     [] by fol notAE Dexists RayWellDefined IntervalRay;
2364       ∡ D B A ≡ ∡ B A D     [] by fol Eexists - Angle_DEF;
2365       ∡ D A B ≡ ∡ D B A     [] by fol AngleSymmetry  ADBncol ANGLE - C5Symmetric;
2366       fol ADBncol - EuclidPropositionI_6;
2367     end;
2368   qed;
2369 `;;
2370
2371 let MidpointExists = theorem `;
2372   ∀A B. ¬(A = B)  ⇒  ∃M. M ∈ Open (A, B)  ∧  seg A M ≡ seg M B
2373
2374   proof
2375     intro_TAC ∀A B, H1;
2376     consider D such that
2377     ¬Collinear A D B  ∧  seg D A ≡ seg D B     [Dexists] by fol H1 IsoscelesExists;
2378     consider F such that
2379     F ∈ int_angle A D B  ∧  ∡ A D F ≡ ∡ F D B     [Fexists] by fol - AngleBisector;
2380     ¬(D = F)     [notDF] by fol - InteriorEZHelp;
2381     consider M such that
2382     M ∈ Open (A, B) ∧  M ∈ ray D F ━ {D}     [Mexists] by fol Fexists Crossbar_THM;
2383     ray D M = ray D F     [] by fol notDF - RayWellDefined;
2384     ∡ A D M ≡ ∡ M D B     [ADMeqMDB] by fol Fexists - Angle_DEF;
2385     M ∈ int_angle A D B     [] by fol Fexists Mexists WholeRayInterior;
2386     ¬(D = M) ∧ ¬Collinear A D M ∧ ¬Collinear B D M     [ADMncol] by fol - InteriorEZHelp InteriorAngleSymmetry;
2387     seg D M ≡ seg D M     [] by fol - SEGMENT C2Reflexive;
2388     A,D,M ≅ B,D,M     [] by fol ADMncol Dexists - ADMeqMDB AngleSymmetry SAS;
2389     fol Mexists - TriangleCong_DEF SegmentSymmetry;
2390   qed;
2391 `;;
2392
2393 let EuclidPropositionI_7short = theorem `;
2394   ∀A B C D a.  ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a  ⇒
2395     ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧ C,D same_side a  ⇒  seg A C ≡ seg A D
2396     ⇒  ¬(seg B C ≡ seg B D)
2397
2398   proof
2399     intro_TAC ∀A B C D a, a_line, Csim_aD, ACeqAD;
2400     ¬(A = C) ∧ ¬(A = D)     [AnotCD] by fol a_line Csim_aD ∉;
2401     assume seg B C ≡ seg B D     [Con] by fol;
2402     seg C B ≡ seg D B  ∧  seg A B ≡ seg A B  ∧  seg A D ≡ seg A D     [segeqs] by fol - SegmentSymmetry a_line AnotCD SEGMENT C2Reflexive;
2403     ¬Collinear A C B  ∧ ¬Collinear A D B     [] by fol a_line I1 Csim_aD Collinear_DEF ∉;
2404     A,C,B ≅ A,D,B     [] by fol - ACeqAD segeqs SSS;
2405     ∡ B A C ≡ ∡ B A D     [] by fol - TriangleCong_DEF;
2406     ray A D = ray A C     [] by fol a_line Csim_aD - C4Uniqueness;
2407     C ∈ ray A D ━ {A}  ∧  D ∈ ray A D ━ {A}     [] by fol AnotCD - EndpointInRay IN_DIFF IN_SING;
2408     C = D     [] by fol AnotCD SEGMENT - ACeqAD segeqs C1;
2409     fol - Csim_aD;
2410   qed;
2411 `;;
2412
2413 let EuclidPropositionI_7Help = theorem `;
2414   ∀A B C D a.  ¬(A = B)  ⇒  Line a ∧ A ∈ a ∧ B ∈ a  ⇒
2415     ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧ C,D same_side a  ⇒  seg A C ≡ seg A D  ⇒
2416     C ∈ int_triangle D A B  ∨  ConvexQuadrilateral A B C D
2417     ⇒  ¬(seg B C ≡ seg B D)
2418
2419   proof
2420     intro_TAC ∀A B C D a, notAB, a_line, Csim_aD, ACeqAD, Int_ConvQuad;
2421     ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D)     [Distinct] by fol a_line Csim_aD ∉ SameSide_DEF;
2422     case_split convex | CintDAB     by fol Int_ConvQuad;
2423     suppose ConvexQuadrilateral A B C D;
2424       A ∈ int_angle B C D  ∧  B ∈ int_angle C D A  ∧  Tetralateral A B C D     [ABint] by fol - ConvexQuad_DEF Quadrilateral_DEF;
2425       ¬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 fol - Tetralateral_DEF CollinearSymmetry ANGLE;
2426       ∡ C D A ≡ ∡ D C A     [CDAeqDCA] by fol angCDB Distinct SEGMENT ACeqAD C2Symmetric IsoscelesCongBaseAngles;
2427       A ∈ int_angle D C B  ∧  ∡ D C A ≡ ∡ D C A  ∧  ∡ C D B ≡ ∡ C D B     [] by fol ABint InteriorAngleSymmetry angCDB ANGLE C5Reflexive;
2428       ∡ D C A <_ang ∡ D C B  ∧  ∡ C D B <_ang ∡ C D A     [] by fol angCDB ABint - AngleOrdering_DEF;
2429       ∡ C D B <_ang ∡ D C B     [] by fol - angCDB CDAeqDCA AngleTrichotomy2 AngleOrderTransitivity;
2430       ¬(∡ D C B ≡ ∡ C D B)     [] by fol - AngleTrichotomy1 angCDB ANGLE C5Symmetric;
2431       fol angCDB - IsoscelesCongBaseAngles;
2432     end;
2433     suppose C ∈ int_triangle D A B;
2434       C ∈ int_angle A D B  ∧  C ∈ int_angle D A B     [CintADB] by fol - IN_InteriorTriangle InteriorAngleSymmetry;
2435       ¬Collinear A D C ∧ ¬Collinear B D C     [ADCncol] by fol CintADB InteriorEZHelp InteriorAngleSymmetry;
2436       ¬Collinear D A C ∧ ¬Collinear C D A ∧ ¬Collinear A C D ∧ ¬Collinear A D C     [DACncol] by fol - CollinearSymmetry;
2437       ¬Collinear B C D ∧ Angle (∡ D C A) ∧ Angle (∡ C D B) ∧ ¬Collinear D C B     [angCDB] by fol ADCncol - CollinearSymmetry ANGLE;
2438       ∡ C D A ≡ ∡ D C A     [CDAeqDCA] by fol DACncol Distinct ADCncol SEGMENT ACeqAD C2Symmetric IsoscelesCongBaseAngles;
2439       consider E such that
2440       D ∈ Open (A, E) ∧ ¬(D = E) ∧ Collinear A D E     [ADE] by fol Distinct B2' B1';
2441       B ∈ int_angle C D E ∧ Collinear D A E     [BintCDE] by fol CintADB - InteriorReflectionInterior CollinearSymmetry;
2442       ¬Collinear C D E     [CDEncol] by fol DACncol - ADE NoncollinearityExtendsToLine;
2443       consider F such that
2444       F ∈ Open (B, D)  ∧  F ∈ ray A C ━ {A}     [Fexists] by fol CintADB Crossbar_THM B1';
2445       F ∈ int_angle B C D     [FintBCD] by fol ADCncol CollinearSymmetry - ConverseCrossbar;
2446       ¬Collinear D C F     [DCFncol] by fol Distinct ADCncol CollinearSymmetry Fexists B1' NoncollinearityExtendsToLine;
2447       Collinear A C F  ∧  F ∈ ray D B ━ {D}  ∧  C ∈ int_angle A D F     [] by fol Fexists IN_DIFF IN_SING IN_Ray B1' IntervalRayEZ CintADB InteriorWellDefined;
2448       C ∈ Open (A, F)     [] by fol - AlternateConverseCrossbar;
2449       ∡ A D C suppl ∡ C D E  ∧  ∡ A C D suppl ∡ D C F     [] by fol ADE DACncol - SupplementaryAngles_DEF;
2450       ∡ C D E ≡ ∡ D C F     [CDEeqDCF] by fol - CDAeqDCA AngleSymmetry SupplementsCongAnglesCong;
2451       ∡ C D B <_ang ∡ C D E     [] by fol angCDB CDEncol BintCDE C5Reflexive AngleOrdering_DEF;
2452       ∡ C D B <_ang ∡ D C F     [CDBlessDCF] by fol - DCFncol ANGLE CDEeqDCF AngleTrichotomy2;
2453       ∡ D C F <_ang ∡ D C B     [] by fol DCFncol ANGLE angCDB FintBCD InteriorAngleSymmetry C5Reflexive AngleOrdering_DEF;
2454       ∡ C D B <_ang ∡ D C B     [] by fol CDBlessDCF - AngleOrderTransitivity;
2455       ¬(∡ D C B ≡ ∡ C D B)     [] by fol - AngleTrichotomy1 angCDB CollinearSymmetry ANGLE C5Symmetric;
2456       fol Distinct ADCncol CollinearSymmetry - IsoscelesCongBaseAngles;
2457     end;
2458   qed;
2459 `;;
2460
2461 let EuclidPropositionI_7 = theorem `;
2462   ∀A B C D a.  ¬(A = B)  ⇒  Line a ∧ A ∈ a ∧ B ∈ a  ⇒
2463     ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧ C,D same_side a  ⇒
2464     seg A C ≡ seg A D
2465    ⇒  ¬(seg B C ≡ seg B D)
2466
2467   proof
2468     intro_TAC ∀A B C D a, notAB, a_line, Csim_aD, ACeqAD;
2469     ¬Collinear A B C ∧ ¬Collinear D A B     [ABCncol] by fol a_line notAB Csim_aD NonCollinearRaa CollinearSymmetry;
2470     ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ A ∉ Open (C, D)     [Distinct] by fol a_line Csim_aD ∉ SameSide_DEF;
2471     ¬Collinear A D C      [ADCncol]
2472     proof
2473       assume Collinear A D C     [Con] by fol;
2474       C ∈ ray A D ━ {A}  ∧  D ∈ ray A D ━ {A}  ∧  seg A D ≡ seg A D     [] by fol Distinct - IN_Ray EndpointInRay IN_DIFF IN_SING SEGMENT C2Reflexive;
2475       fol Distinct SEGMENT - ACeqAD C1 Csim_aD;
2476     qed;
2477     D,C same_side a     [Dsim_aC] by fol a_line Csim_aD SameSideSymmetric;
2478     seg A D ≡ seg A C  ∧  seg B D ≡ seg B D     [ADeqAC] by fol Distinct SEGMENT ACeqAD C2Symmetric C2Reflexive;
2479     ¬Collinear D A C ∧ ¬Collinear C D A ∧ ¬Collinear A C D ∧ ¬Collinear A D C     [DACncol] by fol ADCncol CollinearSymmetry;
2480     ¬(seg B D ≡ seg B C)  ⇒  ¬(seg B C ≡ seg B D)     [BswitchDC] by fol Distinct SEGMENT C2Symmetric;
2481     case_split BDCcol | BDCncol     by fol -;
2482     suppose Collinear B D C;
2483       B ∉ Open (C, D)  ∧  C ∈ ray B D ━ {B}  ∧  D ∈ ray B D ━ {B}     [] by fol a_line Csim_aD SameSide_DEF ∉ Distinct - IN_Ray Distinct IN_DIFF IN_SING EndpointInRay;
2484       fol Distinct SEGMENT - ACeqAD ADeqAC C1 Csim_aD;
2485     end;
2486     suppose ¬Collinear B D C;
2487       Tetralateral A B C D     [] by fol notAB Distinct Csim_aD ABCncol - CollinearSymmetry DACncol Tetralateral_DEF;
2488       ConvexQuadrilateral A B C D  ∨  C ∈ int_triangle D A B  ∨
2489       ConvexQuadrilateral A B D C  ∨  D ∈ int_triangle C A B     [] by fol - a_line Csim_aD  FourChoicesTetralateral InteriorTriangleSymmetry;
2490       fol notAB a_line Csim_aD Dsim_aC ACeqAD ADeqAC - EuclidPropositionI_7Help BswitchDC;
2491     end;
2492   qed;
2493 `;;
2494
2495 let EuclidPropositionI_11 = theorem `;
2496   ∀A B. ¬(A = B)  ⇒  ∃F. Right (∡ A B F)
2497
2498   proof
2499     intro_TAC ∀A B, notAB;
2500     consider C such that
2501     B ∈ Open (A, C)  ∧  seg B C ≡ seg B A     [ABC] by fol notAB SEGMENT C1OppositeRay;
2502     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C     [Distinct] by fol ABC B1';
2503     seg B A ≡ seg B C     [BAeqBC] by fol - SEGMENT ABC C2Symmetric;
2504     consider F such that
2505     ¬Collinear A F C  ∧  seg F A  ≡ seg F C     [Fexists] by fol Distinct IsoscelesExists;
2506     ¬Collinear B F A ∧ ¬Collinear B F C     [BFAncol] by fol - CollinearSymmetry Distinct NoncollinearityExtendsToLine;
2507     ¬Collinear A B F ∧ Angle (∡ A B F)     [angABF] by fol BFAncol CollinearSymmetry ANGLE;
2508     ∡ A B F suppl ∡ F B C     [ABFsuppl] by fol - ABC SupplementaryAngles_DEF;
2509     ¬(B = F)  ∧  seg B F ≡ seg B F     [] by fol BFAncol NonCollinearImpliesDistinct SEGMENT C2Reflexive;
2510     B,F,A ≅ B,F,C     [] by fol BFAncol - BAeqBC Fexists SSS;
2511     ∡ A B F ≡ ∡ F B C     [] by fol - TriangleCong_DEF AngleSymmetry;
2512     fol angABF ABFsuppl - RightAngle_DEF;
2513   qed;
2514 `;;
2515
2516 let DropPerpendicularToLine = theorem `;
2517   ∀P l.  Line l  ∧  P ∉ l  ⇒  ∃E Q. E ∈ l ∧ Q ∈ l ∧ Right (∡ P Q E)
2518
2519   proof
2520     intro_TAC ∀P l, l_line;
2521     consider A B such that
2522     A ∈ l ∧ B ∈ l ∧ ¬(A = B)     [ABl] by fol l_line I2;
2523     ¬Collinear B A P ∧ ¬Collinear P A B ∧ ¬(A = P)     [BAPncol] by fol ABl l_line NonCollinearRaa CollinearSymmetry ∉;
2524     Angle (∡ B A P) ∧ Angle (∡ P A B)     [angBAP] by fol - ANGLE AngleSymmetry;
2525     consider P' such that
2526     ¬(A = P') ∧ P' ∉ l ∧ ¬(P,P' same_side l) ∧ seg A P' ≡ seg A P  ∧  ∡ B A P' ≡ ∡ B A P     [P'exists] by simplify C4OppositeSide - ABl BAPncol l_line;
2527     consider Q such that
2528     Q ∈ l ∧ Q ∈ Open (P, P') ∧ Collinear A B Q     [Qexists] by fol l_line - SameSide_DEF ABl Collinear_DEF;
2529     ¬Collinear B A P'     [BAP'ncol] by fol l_line ABl I1 Collinear_DEF P'exists ∉;
2530     ∡ B A P ≡ ∡ B A P'     [BAPeqBAP'] by fol - ANGLE angBAP P'exists C5Symmetric;
2531     ∃E. E ∈ l  ∧  ¬Collinear P Q E  ∧  ∡ P Q E ≡ ∡ E Q P'     []
2532     proof
2533       assume ¬(A = Q) [notAQ] by fol ABl BAPncol BAPeqBAP' AngleSymmetry;
2534       seg A Q  ≡ seg A Q  ∧  seg A P ≡ seg A P'     [APeqAP'] by fol - SEGMENT C2Reflexive BAPncol P'exists C2Symmetric;
2535       ¬Collinear Q A P' ∧ ¬Collinear Q A P     [QAP'ncol] by fol notAQ l_line ABl Qexists P'exists NonCollinearRaa CollinearSymmetry;
2536       ∡ Q A P ≡ ∡ Q A P'     []
2537       proof
2538         case_split QAB | notQAB     by fol - ∉;
2539         suppose A ∈ Open (Q, B);
2540           ∡ B A P suppl ∡ P A Q   ∧  ∡ B A P' suppl ∡ P' A Q     [] by fol BAPncol BAP'ncol - B1'  SupplementaryAngles_DEF;
2541           fol - BAPeqBAP' SupplementsCongAnglesCong AngleSymmetry;
2542         end;
2543         suppose A ∉ Open (Q, B);
2544           Q ∈ ray A B ━ {A}     [QrayAB_A] by fol ABl Qexists notQAB IN_Ray notAQ IN_DIFF IN_SING;
2545           ray A Q = ray A B     [] by fol - ABl RayWellDefined;
2546           fol notAQ QrayAB_A - BAPeqBAP' Angle_DEF;
2547         end;
2548       qed;
2549       Q,A,P ≅ Q,A,P'     [] by fol QAP'ncol APeqAP' - SAS;
2550       fol - TriangleCong_DEF AngleSymmetry ABl QAP'ncol CollinearSymmetry;
2551     qed;
2552     consider E such that
2553     E ∈ l ∧ ¬Collinear P Q E ∧ ∡ P Q E ≡ ∡ E Q P'     [Eexists] by fol -;
2554     ∡ P Q E suppl ∡ E Q P'  ∧  Right (∡ P Q E)     [] by fol - Qexists SupplementaryAngles_DEF RightAngle_DEF;
2555     fol Eexists Qexists -;
2556   qed;
2557 `;;
2558
2559 let EuclidPropositionI_14 = theorem `;
2560   ∀A B C D l.  Line l ∧ A ∈ l ∧ B ∈ l ∧ ¬(A = B)  ⇒
2561     C ∉ l ∧ D ∉ l ∧ ¬(C,D same_side l)  ⇒ ∡ C B A suppl ∡ A B D
2562     ⇒  B ∈ Open (C, D)
2563
2564   proof
2565     intro_TAC ∀A B C D l, l_line, Cnsim_lD, CBAsupplABD;
2566     ¬(B = C) ∧ ¬(B = D) ∧ ¬Collinear C B A     [Distinct] by fol l_line Cnsim_lD ∉ I1 Collinear_DEF;
2567     consider E such that
2568     B ∈ Open (C, E)     [CBE] by fol Distinct B2';
2569     E ∉ l ∧ ¬(C,E same_side l)     [Csim_lE] by fol l_line ∉ - BetweenLinear Cnsim_lD SameSide_DEF;
2570     D,E same_side l     [Dsim_lE] by fol l_line Cnsim_lD - AtMost2Sides;
2571     ∡ C B A suppl ∡ A B E     [] by fol Distinct CBE SupplementaryAngles_DEF;
2572     ∡ A B D ≡ ∡ A B E     [] by fol CBAsupplABD - SupplementUnique;
2573     ray B E = ray B D     [] by fol l_line Csim_lE Cnsim_lD Dsim_lE - C4Uniqueness;
2574     D ∈ ray B E ━ {B}     [] by fol Distinct - EndpointInRay IN_DIFF IN_SING;
2575     fol CBE - OppositeRaysIntersect1pointHelp B1';
2576   qed;
2577 `;;
2578
2579 (* Euclid's Proposition I.15 *)
2580
2581 let VerticalAnglesCong = theorem `;
2582   ∀A B O A' B'.  ¬Collinear A O B  ⇒ O ∈ Open (A, A')  ∧  O ∈ Open (B, B')
2583     ⇒  ∡ B O A' ≡ ∡ B' O A
2584
2585   proof
2586     intro_TAC ∀A B O A' B', H1, H2;
2587     ∡ A O B suppl ∡ B O A'     [AOBsupplBOA'] by fol H1 H2 SupplementaryAngles_DEF;
2588     ∡ B O A suppl ∡ A O B'     [] by fol H1 CollinearSymmetry H2 SupplementaryAngles_DEF;
2589     fol AOBsupplBOA' - AngleSymmetry SupplementUnique;
2590   qed;
2591 `;;
2592
2593 let EuclidPropositionI_16 = theorem `;
2594   ∀A B C D. ¬Collinear A B C  ∧  C ∈ Open (B, D)
2595     ⇒  ∡ B A C <_ang ∡ D C A
2596
2597   proof
2598     intro_TAC ∀A B C D, H1 H2;
2599     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2600     consider l such that
2601     Line l ∧ A ∈ l ∧ C ∈ l     [l_line] by fol Distinct I1;
2602     consider m such that
2603     Line m ∧ B ∈ m ∧ C ∈ m     [m_line] by fol Distinct I1;
2604     D ∈ m     [Dm] by fol m_line H2 BetweenLinear;
2605     consider E such that
2606     E ∈ Open (A, C) ∧ seg A E ≡ seg E C     [AEC] by fol Distinct MidpointExists;
2607     ¬(A = E) ∧ ¬(E = C) ∧ Collinear A E C ∧ ¬(B = E)     [AECcol] by fol - B1' H1;
2608     E ∈ l     [El] by fol l_line AEC BetweenLinear;
2609     consider F such that
2610     E ∈ Open (B, F) ∧ seg E F ≡ seg E B     [BEF] by fol AECcol SEGMENT C1OppositeRay;
2611     ¬(B = E) ∧ ¬(B = F) ∧ ¬(E = F) ∧ Collinear B E F     [BEF'] by fol BEF B1';
2612     B ∉ l     [notBl] by fol l_line Distinct I1 Collinear_DEF H1 ∉;
2613     ¬Collinear A E B ∧ ¬Collinear C E B     [AEBncol] by fol AECcol l_line El notBl NonCollinearRaa CollinearSymmetry;
2614     Angle (∡ B A E)     [angBAE] by fol - CollinearSymmetry ANGLE;
2615     ¬Collinear C E F     [CEFncol] by fol AEBncol BEF' CollinearSymmetry NoncollinearityExtendsToLine;
2616     ∡ B E A ≡ ∡ F E C     [BEAeqFEC] by fol AEBncol AEC B1' BEF VerticalAnglesCong;
2617     seg E A ≡ seg E C  ∧  seg E B ≡ seg E F     [] by fol AEC SegmentSymmetry AECcol BEF'  SEGMENT BEF C2Symmetric;
2618     A,E,B ≅ C,E,F     [] by fol AEBncol CEFncol - BEAeqFEC AngleSymmetry SAS;
2619     ∡ B A E ≡ ∡ F C E     [BAEeqFCE] by fol - TriangleCong_DEF;
2620     ¬Collinear E C D     [ECDncol] by fol AEBncol H2 B1' CollinearSymmetry NoncollinearityExtendsToLine;
2621     F ∉ l ∧ D ∉ l     [notFl] by fol l_line El Collinear_DEF CEFncol - ∉;
2622     F ∈ ray B E ━ {B}  ∧  E ∉ m     [] by fol BEF IntervalRayEZ m_line Collinear_DEF AEBncol ∉;
2623     F ∉ m  ∧  F,E same_side m     [Fsim_mE] by fol m_line - RaySameSide;
2624     ¬(B,F same_side l)  ∧  ¬(B,D same_side l)     [] by fol El l_line BEF H2 SameSide_DEF;
2625     F,D same_side l     [] by fol l_line notBl notFl - AtMost2Sides;
2626     F ∈ int_angle E C D     [] by fol ECDncol l_line El m_line Dm notFl Fsim_mE - IN_InteriorAngle;
2627     ∡ B A E <_ang ∡ E C D     [BAElessECD] by fol angBAE ECDncol - BAEeqFCE AngleSymmetry AngleOrdering_DEF;
2628     ray A E = ray A C  ∧  ray C E = ray C A     [] by fol AEC B1' IntervalRay;
2629     ∡ B A C <_ang ∡ A C D     [] by fol BAElessECD - Angle_DEF;
2630     fol - AngleSymmetry;
2631   qed;
2632 `;;
2633
2634 let ExteriorAngle = theorem `;
2635   ∀A B C D.  ¬Collinear A B C  ∧  C ∈ Open (B, D)
2636     ⇒  ∡ A B C <_ang ∡ A C D
2637
2638   proof
2639     intro_TAC ∀A B C D, H1 H2;
2640     ¬(C = D) ∧ C ∈ Open (D, B) ∧ Collinear B C D     [H2'] by fol H2 BetweenLinear B1';
2641     ¬Collinear B A C ∧ ¬(A = C)     [BACncol] by fol H1 CollinearSymmetry NonCollinearImpliesDistinct;
2642     consider E such that
2643     C ∈ Open (A, E)     [ACE] by fol - B2';
2644     ¬(C = E) ∧ C ∈ Open (E, A) ∧ Collinear A C E     [ACE'] by fol - B1';
2645     ¬Collinear A C D ∧ ¬Collinear D C E     [DCEncol] by fol H1 CollinearSymmetry H2' - NoncollinearityExtendsToLine;
2646     ∡ A B C <_ang ∡ E C B     [ABClessECB] by fol BACncol ACE EuclidPropositionI_16;
2647     ∡ E C B ≡ ∡ A C D     [] by fol DCEncol ACE' H2' VerticalAnglesCong;
2648     fol ABClessECB DCEncol ANGLE - AngleTrichotomy2;
2649   qed;
2650 `;;
2651
2652 let EuclidPropositionI_17 = theorem `;
2653   ∀A B C α β γ.  ¬Collinear A B C  ∧  α = ∡ A B C  ∧  β = ∡ B C A  ⇒
2654     β suppl γ
2655     ⇒  α <_ang γ
2656
2657   proof
2658     intro_TAC ∀A B C α β γ, H1, H2;
2659     Angle γ     [angγ] by fol H2 SupplementImpliesAngle;
2660     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2661     ¬Collinear B A C ∧ ¬Collinear A C B     [BACncol] by fol H1 CollinearSymmetry;
2662     consider D such that
2663     C ∈ Open (A, D)     [ACD] by fol Distinct B2';
2664     ∡ A B C <_ang ∡ D C B     [ABClessDCB] by fol BACncol ACD EuclidPropositionI_16;
2665     β suppl ∡ B C D     [] by fol - H1 AngleSymmetry BACncol ACD SupplementaryAngles_DEF;
2666     ∡ B C D ≡ γ     [] by fol H2 - SupplementUnique;
2667     fol ABClessDCB H1 AngleSymmetry angγ - AngleTrichotomy2;
2668   qed;
2669 `;;
2670
2671 let EuclidPropositionI_18 = theorem `;
2672   ∀A B C.  ¬Collinear A B C  ∧  seg A C <__ seg A B
2673     ⇒  ∡ A B C <_ang ∡ B C A
2674
2675   proof
2676     intro_TAC ∀A B C, H1 H2;
2677     ¬(A = B) ∧ ¬(A = C)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2678     consider D such that
2679     D ∈ Open (A, B) ∧ seg A C ≡ seg A D     [ADB] by fol Distinct SEGMENT H2 SegmentOrderingUse;
2680     ¬(D = A) ∧ ¬(D = B) ∧ D ∈ Open (B, A) ∧ Collinear A D B ∧ ray B D = ray B A     [ADB'] by fol - B1' IntervalRay;
2681     D ∈ int_angle A C B  ∧ ¬Collinear A C B      [DintACB] by fol H1 CollinearSymmetry ADB ConverseCrossbar;
2682     ¬Collinear D A C ∧ ¬Collinear C B D ∧ ¬Collinear C D A     [DACncol] by fol H1 CollinearSymmetry ADB' NoncollinearityExtendsToLine;
2683     seg A D ≡ seg A C     [] by fol ADB' Distinct SEGMENT ADB C2Symmetric;
2684     ∡ C D A ≡ ∡ A C D     [] by fol DACncol - IsoscelesCongBaseAngles AngleSymmetry;
2685     ∡ C D A <_ang ∡ A C B     [CDAlessACB] by fol DACncol ANGLE H1 DintACB - AngleOrdering_DEF;
2686     ∡ B D C suppl ∡ C D A     [] by fol DACncol CollinearSymmetry ADB' SupplementaryAngles_DEF;
2687     ∡ C B D <_ang ∡ C D A     [] by fol DACncol - EuclidPropositionI_17;
2688     ∡ C B D <_ang ∡ A C B     [] by fol - CDAlessACB AngleOrderTransitivity;
2689     fol - ADB' Angle_DEF AngleSymmetry;
2690   qed;
2691 `;;
2692
2693 let EuclidPropositionI_19 = theorem `;
2694   ∀A B C. ¬Collinear A B C  ∧  ∡ A B C <_ang ∡ B C A
2695     ⇒  seg A C  <__ seg A B
2696
2697   proof
2698     intro_TAC ∀A B C, H1 H2;
2699     ¬Collinear B A C ∧ ¬Collinear B C A ∧ ¬Collinear A C B     [BACncol] by fol H1 CollinearSymmetry;
2700     ¬(A = B) ∧ ¬(A = C)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2701     assume ¬(seg A C  <__ seg A B)     [Con] by fol;
2702     seg A B ≡ seg A C   ∨  seg A B  <__ seg A C     [] by fol Distinct SEGMENT - SegmentTrichotomy;
2703     case_split cong | less     by fol -;
2704     suppose seg A B ≡ seg A C;
2705       ∡ C B A ≡ ∡ B C A     [] by fol BACncol - IsoscelesCongBaseAngles;
2706       fol - AngleSymmetry H2 AngleTrichotomy1;
2707     end;
2708     suppose seg A B  <__ seg A C;
2709       ∡ A C B <_ang ∡ C B A     [] by fol BACncol - EuclidPropositionI_18;
2710       fol H1 BACncol ANGLE - AngleSymmetry H2 AngleTrichotomy;
2711     end;
2712   qed;
2713 `;;
2714
2715 let EuclidPropositionI_20 = theorem `;
2716   ∀A B C D. ¬Collinear A B C  ⇒  A ∈ Open (B, D)  ∧  seg A D ≡ seg A C
2717     ⇒  seg B C <__ seg B D
2718
2719   proof
2720     intro_TAC ∀A B C D, H1, H2;
2721     ¬(B = D) ∧ ¬(A = D) ∧ A ∈ Open (D, B) ∧ Collinear B A D ∧ ray D A = ray D B     [BAD'] by fol H2 B1' IntervalRay;
2722     ¬Collinear C A D     [CADncol] by fol H1 CollinearSymmetry BAD' NoncollinearityExtendsToLine;
2723     ¬Collinear D C B ∧ ¬Collinear B D C     [DCBncol] by fol H1 CollinearSymmetry BAD' NoncollinearityExtendsToLine;
2724     Angle (∡ C D A)     [angCDA] by fol CADncol CollinearSymmetry ANGLE;
2725     ∡ C D A ≡ ∡ D C A     [CDAeqDCA] by fol CADncol CollinearSymmetry H2 IsoscelesCongBaseAngles;
2726     A ∈ int_angle D C B     [] by fol DCBncol BAD' ConverseCrossbar;
2727     ∡ C D A <_ang ∡ D C B     [] by fol angCDA DCBncol - CDAeqDCA AngleOrdering_DEF;
2728     ∡ B D C <_ang ∡ D C B     [] by fol - BAD' Angle_DEF AngleSymmetry;
2729     fol DCBncol - EuclidPropositionI_19;
2730   qed;
2731 `;;
2732
2733 let EuclidPropositionI_21 = theorem `;
2734   ∀A B C D. ¬Collinear A B C  ∧  D ∈ int_triangle A B C
2735     ⇒  ∡ A B C <_ang ∡ C D A
2736
2737   proof
2738     intro_TAC ∀A B C D, H1 H2;
2739     ¬(B = A) ∧ ¬(B = C) ∧ ¬(A = C)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2740     D ∈ int_angle B A C  ∧  D ∈ int_angle C B A     [DintTri] by fol H2 IN_InteriorTriangle InteriorAngleSymmetry;
2741     consider E such that
2742     E ∈ Open (B, C) ∧ E ∈ ray A D ━ {A}     [BEC] by fol - Crossbar_THM;
2743     ¬(B = E) ∧ ¬(E = C) ∧ Collinear B E C  ∧  Collinear A D E      [BEC'] by fol - B1' IN_Ray IN_DIFF IN_SING;
2744     ray B E = ray B C  ∧  E ∈ ray B C ━ {B}     [rBErBC] by fol BEC IntervalRay IntervalRayEZ;
2745     D ∈ int_angle A B E     [DintABE] by fol DintTri - InteriorAngleSymmetry InteriorWellDefined;
2746     D ∈ Open (A, E)     [ADE] by fol BEC' - AlternateConverseCrossbar;
2747     ray E D = ray E A     [rEDrEA] by fol - B1' IntervalRay;
2748     ¬Collinear A B E ∧ ¬Collinear B E A  ∧ ¬Collinear C B D ∧ ¬(A = D)     [ABEncol] by fol DintABE IN_InteriorAngle CollinearSymmetry DintTri InteriorEZHelp;
2749     ¬Collinear E D C ∧ ¬Collinear C E D     [EDCncol] by fol - CollinearSymmetry BEC'  NoncollinearityExtendsToLine;
2750     ∡ A B E <_ang ∡ A E C  ∧  ∡ C E D = ∡ D E C     [] by fol ABEncol BEC ExteriorAngle AngleSymmetry;
2751     ∡ A B C <_ang ∡ C E D     [ABClessAEC] by fol - rBErBC rEDrEA Angle_DEF;
2752     ∡ C E D  <_ang  ∡ C D A     [] by fol EDCncol ADE B1' ExteriorAngle;
2753     fol ABClessAEC - AngleOrderTransitivity;
2754   qed;
2755 `;;
2756
2757 let AngleTrichotomy3 = theorem `;
2758   ∀α β γ.  α <_ang β  ∧  Angle γ  ∧  γ ≡ α  ⇒  γ <_ang β
2759
2760   proof
2761     intro_TAC ∀α β γ, H1;
2762     consider A O B G such that
2763     Angle α ∧ ¬Collinear A O B ∧ β = ∡ A O B ∧ G ∈ int_angle A O B ∧ α ≡ ∡ A O G     [H1'] by fol H1 AngleOrdering_DEF;
2764     ¬Collinear A O G     [] by fol - InteriorEZHelp;
2765     γ ≡ ∡ A O G     [] by fol H1 H1' - ANGLE C5Transitive;
2766     fol H1 H1' - AngleOrdering_DEF;
2767   qed;
2768 `;;
2769
2770 let InteriorCircleConvexHelp = theorem `;
2771   ∀O A B C. ¬Collinear A O C  ⇒  B ∈ Open (A, C)  ⇒
2772     seg O A <__ seg O C  ∨  seg O A ≡ seg O C
2773     ⇒  seg O B <__ seg O C
2774
2775   proof
2776     intro_TAC ∀O A B C, H1, H2, H3;
2777     ¬Collinear O C A ∧ ¬Collinear C O A ∧ ¬(O = A) ∧ ¬(O = C)     [H1'] by fol H1 CollinearSymmetry NonCollinearImpliesDistinct;
2778     ray A B = ray A C  ∧  ray C B = ray C A     [equal_rays] by fol H2 IntervalRay B1';
2779     ∡ O C A <_ang ∡ C A O  ∨  ∡ O C A ≡ ∡ C A O     []
2780     proof
2781       assume seg O A ≡ seg O C [seg_eq] by fol H3 H1' EuclidPropositionI_18;
2782       seg O C ≡ seg O A     [] by fol H1' SEGMENT - C2Symmetric;
2783       fol H1' - IsoscelesCongBaseAngles AngleSymmetry;
2784     qed;
2785     ∡ O C B <_ang ∡ B A O  ∨  ∡ O C B ≡ ∡ B A O     [] by fol - equal_rays Angle_DEF;
2786     ∡ B C O <_ang ∡ O A B  ∨  ∡ B C O ≡ ∡ O A B     [BCOlessOAB] by fol - AngleSymmetry;
2787     ¬Collinear O A B ∧ ¬Collinear B C O ∧ ¬Collinear O C B     [OABncol] by fol H1 CollinearSymmetry H2 B1' NoncollinearityExtendsToLine;
2788     ∡ O A B <_ang ∡ O B C     [] by fol - H2 ExteriorAngle;
2789     ∡ B C O <_ang ∡ O B C     [] by fol BCOlessOAB - AngleOrderTransitivity OABncol ANGLE - AngleTrichotomy3;
2790     fol OABncol - AngleSymmetry EuclidPropositionI_19;
2791   qed;
2792 `;;
2793
2794 let InteriorCircleConvex = theorem `;
2795   ∀O R A B C.  ¬(O = R)  ⇒  B ∈ Open (A, C)  ⇒
2796     A ∈ int_circle O R  ∧  C ∈ int_circle O R
2797     ⇒  B ∈ int_circle O R
2798
2799   proof
2800     intro_TAC ∀O R A B C, H1, H2, H3;
2801     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ B ∈ Open (C, A)     [H2'] by fol H2 B1';
2802     (A = O  ∨  seg O A <__ seg O R)  ∧  (C = O  ∨  seg O C <__ seg O R)     [ACintOR] by fol H3 H1 IN_InteriorCircle;
2803     case_split OAC | OnotAC     by fol -;
2804     suppose O = A ∨ O = C;
2805       B ∈ Open (O, C)  ∨  B ∈ Open (O, A)     [] by fol - H2 B1';
2806       seg O B <__ seg O A ∧ ¬(O = A)  ∨  seg O B <__ seg O C ∧ ¬(O = C)     [] by fol - B1' SEGMENT C2Reflexive  SegmentOrdering_DEF;
2807       seg O B <__ seg O R     [] by fol - ACintOR SegmentOrderTransitivity;
2808       fol - H1 IN_InteriorCircle;
2809     end;
2810     suppose ¬(O = A) ∧ ¬(O = C);
2811       case_split AOCncol | AOCcol     by fol -;
2812       suppose ¬Collinear A O C;
2813         seg O A <__ seg O C  ∨  seg O A ≡ seg O C  ∨  seg O C <__ seg O A     [] by fol OnotAC SEGMENT  SegmentTrichotomy;
2814         seg O B <__ seg O C  ∨  seg O B <__ seg O A     [] by fol AOCncol H2 - InteriorCircleConvexHelp CollinearSymmetry B1';
2815         fol OnotAC ACintOR - SegmentOrderTransitivity H1 IN_InteriorCircle;
2816       end;
2817       suppose Collinear A O C;
2818         consider l such that
2819         Line l ∧ A ∈ l ∧ C ∈ l     [l_line] by fol H2' I1;
2820         Collinear B A O ∧ Collinear B C O     [OABCcol] by fol - H2 BetweenLinear H2' AOCcol CollinearLinear Collinear_DEF;
2821         B ∉ Open (O, A) ∧ B ∉ Open (O, C)  ⇒  B = O     []
2822         proof
2823           intro_TAC Assumption;
2824           O ∈ ray B A ∩ ray B C     [] by fol H2' OABCcol - IN_Ray IN_INTER;
2825           fol - H2 OppositeRaysIntersect1point IN_SING;
2826         qed;
2827         B ∈ Open (O, A)  ∨  B ∈ Open (O, C)  ∨  B = O     [] by fol - ∉;
2828         seg O B <__ seg O A  ∨  seg O B <__ seg O C  ∨  B = O     [] by fol - B1' SEGMENT C2Reflexive  SegmentOrdering_DEF;
2829         seg O B <__ seg O R  ∨  B = O     [] by fol - ACintOR OnotAC SegmentOrderTransitivity;
2830         fol - H1 IN_InteriorCircle;
2831       end;
2832     end;
2833   qed;
2834 `;;
2835
2836 let SegmentTrichotomy3 = theorem `;
2837   ∀s t u.  s <__ t  ∧  Segment u  ∧  u ≡ s  ⇒  u <__ t
2838
2839   proof
2840     intro_TAC ∀s t u, H1;
2841     consider C D X such that
2842     Segment s ∧ t = seg C D ∧ X ∈ Open (C, D) ∧ s ≡ seg C X ∧ ¬(C = X)     [H1'] by fol H1 SegmentOrdering_DEF B1';
2843     u ≡ seg C X     [] by fol H1 - SEGMENT C2Transitive;
2844     fol H1 H1' - SegmentOrdering_DEF;
2845   qed;
2846 `;;
2847
2848 let EuclidPropositionI_24Help = theorem `;
2849   ∀O A C O' D M.  ¬Collinear A O C ∧ ¬Collinear D O' M  ⇒
2850     seg O' D ≡ seg O A  ∧  seg O' M ≡ seg O C  ⇒  ∡ D O' M <_ang ∡ A O C  ⇒
2851     seg O A <__ seg O C  ∨  seg O A ≡ seg O C
2852     ⇒  seg D M <__ seg A C
2853
2854   proof
2855     intro_TAC ∀O A C O' D M, H1, H2, H3, H4;
2856     consider K such that
2857     K ∈ int_angle A O C ∧ ∡ D O' M ≡ ∡ A O K     [KintAOC] by fol H1 ANGLE H3 AngleOrderingUse;
2858     ¬(O = C) ∧ ¬(D = M) ∧ ¬(O' = M) ∧ ¬(O = K)     [Distinct] by fol H1 NonCollinearImpliesDistinct - InteriorEZHelp;
2859     consider B such that
2860     B ∈ ray O K ━ {O}  ∧  seg O B ≡ seg O C     [BrOK] by fol Distinct SEGMENT - C1;
2861     ray O B = ray O K     [] by fol Distinct - RayWellDefined;
2862     ∡ D O' M ≡ ∡ A O B     [DO'MeqAOB] by fol KintAOC - Angle_DEF;
2863     B ∈ int_angle A O C     [BintAOC] by fol KintAOC BrOK WholeRayInterior;
2864     ¬(B = O) ∧ ¬Collinear A O B     [AOBncol] by fol - InteriorEZHelp;
2865     seg O C ≡ seg O B     [OCeqOB] by fol Distinct - SEGMENT BrOK C2Symmetric;
2866     seg O' M ≡ seg O B     [] by fol Distinct SEGMENT AOBncol H2 - C2Transitive;
2867     D,O',M ≅ A,O,B     [] by fol H1 AOBncol H2 - DO'MeqAOB SAS;
2868     seg D M ≡ seg A B     [DMeqAB] by fol - TriangleCong_DEF;
2869     consider G such that
2870     G ∈ Open (A, C)  ∧  G ∈ ray O B ━ {O}  ∧  ¬(G = O)     [AGC] by fol BintAOC Crossbar_THM B1' IN_DIFF IN_SING;
2871     Segment (seg O G) ∧ ¬(O = B)     [notOB] by fol - SEGMENT BrOK IN_DIFF IN_SING;
2872     seg O G <__ seg O C     [] by fol H1 AGC H4 InteriorCircleConvexHelp;
2873     seg O G <__ seg O B     [] by fol - OCeqOB BrOK SEGMENT SegmentTrichotomy2 IN_DIFF IN_SING;
2874     consider G' such that
2875     G' ∈ Open (O, B)  ∧  seg O G ≡ seg O G'     [OG'B] by fol notOB - SegmentOrderingUse;
2876     ¬(G' = O)  ∧  seg O G' ≡ seg O G'  ∧  Segment (seg O G')     [notG'O] by fol - B1' SEGMENT C2Reflexive SEGMENT;
2877     G' ∈ ray O B ━ {O}     [] by fol OG'B IntervalRayEZ;
2878     G' = G  ∧  G ∈ Open (B, O)     [] by fol notG'O notOB - AGC OG'B C1 B1';
2879     ConvexQuadrilateral B A O C     [] by fol H1 - AGC DiagonalsIntersectImpliesConvexQuad;
2880     A ∈ int_angle O C B  ∧  O ∈ int_angle C B A  ∧  Quadrilateral B A O C     [OintCBA] by fol - ConvexQuad_DEF;
2881     A ∈ int_angle B C O     [AintBCO] by fol - InteriorAngleSymmetry;
2882     Tetralateral B A O C     [] by fol OintCBA Quadrilateral_DEF;
2883     ¬Collinear C B A  ∧ ¬Collinear B C O ∧ ¬Collinear C O B ∧ ¬Collinear C B O     [BCOncol] by fol - Tetralateral_DEF CollinearSymmetry;
2884     ∡ B C O ≡ ∡ C B O     [BCOeqCBO] by fol - OCeqOB IsoscelesCongBaseAngles;
2885     ¬Collinear B C A ∧ ¬Collinear A C B     [ACBncol] by fol AintBCO InteriorEZHelp CollinearSymmetry;
2886     ∡ B C A ≡ ∡ B C A  ∧  Angle (∡ B C A)  ∧  ∡ C B O ≡ ∡ C B O     [CBOref] by fol - ANGLE BCOncol C5Reflexive;
2887     ∡ B C A <_ang ∡ B C O     [] by fol - BCOncol ANGLE AintBCO AngleOrdering_DEF;
2888     ∡ B C A <_ang ∡ C B O     [BCAlessCBO] by fol - BCOncol ANGLE BCOeqCBO AngleTrichotomy2;
2889     ∡ C B O <_ang ∡ C B A     [] by fol BCOncol ANGLE OintCBA CBOref AngleOrdering_DEF;
2890     ∡ A C B <_ang ∡ C B A     [] by fol BCAlessCBO - AngleOrderTransitivity AngleSymmetry;
2891     seg A B <__ seg A C     [] by fol ACBncol - EuclidPropositionI_19;
2892     fol - Distinct SEGMENT DMeqAB SegmentTrichotomy3;
2893  qed;
2894 `;;
2895
2896 let EuclidPropositionI_24 = theorem `;
2897   ∀O A C O' D M. ¬Collinear A O C ∧ ¬Collinear D O' M  ⇒
2898     seg O' D ≡ seg O A ∧ seg O' M ≡ seg O C  ⇒  ∡ D O' M <_ang ∡ A O C
2899     ⇒  seg D M <__ seg A C
2900
2901   proof
2902     intro_TAC ∀O A C O' D M, H1, H2, H3;
2903     ¬(O = A) ∧ ¬(O = C) ∧ ¬Collinear C O A ∧ ¬Collinear M O' D     [Distinct] by fol H1 NonCollinearImpliesDistinct CollinearSymmetry;
2904     seg O A ≡ seg O C  ∨  seg O A <__ seg O C  ∨  seg O C <__ seg O A     [3pos] by fol  - SEGMENT SegmentTrichotomy;
2905     assume seg O C <__ seg O A [H4] by fol 3pos H1 H2 H3 EuclidPropositionI_24Help;
2906     ∡ M O' D <_ang ∡ C O A     [] by fol H3 AngleSymmetry;
2907     fol Distinct H3 AngleSymmetry H2 H4 EuclidPropositionI_24Help SegmentSymmetry;
2908   qed;
2909 `;;
2910
2911 let EuclidPropositionI_25 = theorem `;
2912   ∀O A C O' D M.  ¬Collinear A O C ∧ ¬Collinear D O' M  ⇒
2913     seg O' D ≡ seg O A ∧ seg O' M ≡ seg O C  ⇒  seg D M <__ seg A C
2914     ⇒  ∡ D O' M <_ang ∡ A O C
2915
2916   proof
2917     intro_TAC ∀O A C O' D M, H1, H2, H3;
2918     ¬(O = A) ∧ ¬(O = C) ∧ ¬(A = C) ∧ ¬(D = M) ∧ ¬(O' = D) ∧ ¬(O' = M)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2919     assume ¬(∡ D O' M <_ang ∡ A O C)     [Contradiction] by fol;
2920     ∡ D O' M ≡ ∡ A O C  ∨  ∡ A O C <_ang ∡ D O' M     [] by fol H1 ANGLE - AngleTrichotomy;
2921     case_split Cong | Con     by fol -;
2922     suppose ∡ D O' M ≡ ∡ A O C;
2923       D,O',M ≅ A,O,C     [] by fol H1 H2 - SAS;
2924       seg D M ≡ seg A C     [] by fol - TriangleCong_DEF;
2925       fol Distinct SEGMENT - H3 SegmentTrichotomy;
2926     end;
2927     suppose ∡ A O C <_ang ∡ D O' M;
2928       seg O A ≡ seg O' D  ∧  seg O C  ≡ seg O' M     [H2'] by fol Distinct SEGMENT H2 C2Symmetric;
2929       seg A C <__ seg D M     [] by fol H1 - Con EuclidPropositionI_24;
2930       fol Distinct SEGMENT - H3 SegmentTrichotomy;
2931     end;
2932   qed;
2933 `;;
2934
2935 let AAS = theorem `;
2936   ∀A B C A' B' C'. ¬Collinear A B C ∧ ¬Collinear A' B' C'  ⇒
2937     ∡ A B C ≡ ∡ A' B' C'  ∧  ∡ B C A ≡ ∡ B' C' A'  ⇒  seg A B ≡ seg A' B'
2938     ⇒  A,B,C ≅ A',B',C'
2939
2940   proof
2941     intro_TAC ∀A B C A' B' C', H1, H2, H3;
2942     ¬(A = B) ∧ ¬(B = C) ∧ ¬(B' = C')     [Distinct] by fol H1 NonCollinearImpliesDistinct;
2943     consider G such that
2944     G ∈ ray B C ━ {B} ∧ seg B G ≡ seg B' C'     [Gexists] by fol Distinct SEGMENT C1;
2945     ¬(G = B)  ∧  B ∉ Open (G, C)  ∧ Collinear G B C     [notGBC] by fol - IN_Ray CollinearSymmetry IN_DIFF IN_SING;
2946     ¬Collinear A B G ∧ ¬Collinear B G A     [ABGncol] by fol H1 notGBC CollinearSymmetry NoncollinearityExtendsToLine;
2947     ray B G = ray B C     [] by fol Distinct Gexists RayWellDefined;
2948     ∡ A B G = ∡ A B C     [] by fol Distinct - Angle_DEF;
2949     A,B,G ≅ A',B',C'     [ABG≅A'B'C'] by fol H1 ABGncol H3 SegmentSymmetry H2 - Gexists SAS;
2950     ∡ B G A ≡ ∡ B' C' A'     [BGAeqB'C'A'] by fol - TriangleCong_DEF;
2951     ¬Collinear B C A  ∧ ¬Collinear B' C' A'     [BCAncol] by fol H1 CollinearSymmetry;
2952     ∡ B' C' A' ≡ ∡ B C A  ∧  ∡ B C A ≡ ∡ B C A     [BCArefl] by fol - ANGLE H2 C5Symmetric C5Reflexive;
2953     ∡ B G A ≡ ∡ B C A     [BGAeqBCA] by fol ABGncol BCAncol ANGLE BGAeqB'C'A' - C5Transitive;
2954     assume ¬(G = C)     [notGC] by fol BGAeqBCA ABG≅A'B'C';
2955     ¬Collinear A C G ∧ ¬Collinear A G C     [ACGncol] by fol H1 notGBC - CollinearSymmetry NoncollinearityExtendsToLine;
2956     C ∈ Open (B, G) ∨ G ∈ Open (C, B)     [] by fol notGBC notGC Distinct B3' ∉;
2957     case_split BCG |  CGB by fol -;
2958     suppose C ∈ Open (B, G) ;
2959       C ∈ Open (G, B)  ∧ ray G C = ray G B     [rGCrBG] by fol - B1' IntervalRay;
2960       ∡ A G C <_ang ∡ A C B     [] by fol ACGncol - ExteriorAngle;
2961       ∡ B G A <_ang ∡ B C A     [] by fol - rGCrBG Angle_DEF AngleSymmetry AngleSymmetry;
2962       fol ABGncol BCAncol ANGLE - AngleSymmetry BGAeqBCA AngleTrichotomy;
2963     end;
2964     suppose G ∈ Open (C, B);
2965       ray C G = ray C B  ∧  ∡ A C G <_ang ∡ A G B     [] by fol - IntervalRay ACGncol ExteriorAngle;
2966       ∡ A C B <_ang ∡ B G A     [] by fol - Angle_DEF AngleSymmetry;
2967       ∡ B C A <_ang ∡ B C A     [] by fol - BCAncol ANGLE BGAeqBCA AngleTrichotomy2 AngleSymmetry;
2968       fol - BCArefl AngleTrichotomy1;
2969     end;
2970   qed;
2971 `;;
2972
2973 let ParallelSymmetry = theorem `;
2974   ∀l k. l ∥ k  ⇒  k ∥ l
2975   by fol PARALLEL INTER_COMM`;;
2976
2977 let AlternateInteriorAngles = theorem `;
2978   ∀A B C E l m t.  Line l ∧ A ∈ l ∧ E ∈ l  ⇒
2979     Line m ∧ B ∈ m ∧ C ∈ m  ⇒  Line t ∧ A ∈ t ∧ B ∈ t  ⇒
2980     ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t  ⇒
2981     ¬(C,E same_side t)  ⇒  ∡ E A B ≡ ∡ C B A
2982     ⇒  l ∥ m
2983
2984   proof
2985     intro_TAC ∀A B C E l m t, l_line, m_line, t_line, Distinct, Cnsim_tE, AltIntAngCong;
2986     ¬Collinear E A B ∧ ¬Collinear C B A     [EABncol] by fol t_line Distinct NonCollinearRaa CollinearSymmetry;
2987     B ∉ l ∧ A ∉ m     [notAmBl] by fol l_line m_line Collinear_DEF - ∉;
2988     assume ¬(l ∥ m)     [Con] by fol;
2989     ¬(l ∩ m = ∅)     [] by fol - l_line m_line PARALLEL;
2990     consider G such that
2991     G ∈ l ∧ G ∈ m     [Glm] by fol - MEMBER_NOT_EMPTY IN_INTER;
2992     ¬(G = A) ∧ ¬(G = B) ∧ Collinear B G C ∧ Collinear B C G ∧ Collinear A E G ∧ Collinear A G E     [GnotAB] by fol - notAmBl ∉ m_line l_line Collinear_DEF;
2993     ¬Collinear A G B ∧ ¬Collinear B G A ∧ G ∉ t      [AGBncol]  by fol EABncol CollinearSymmetry - NoncollinearityExtendsToLine t_line Collinear_DEF ∉;
2994     ¬(E,C same_side t)     [Ensim_tC] by fol t_line - Distinct Cnsim_tE SameSideSymmetric;
2995     E ∈ l ━ {A}  ∧  G ∈ l ━ {A}     [] by fol l_line Glm Distinct GnotAB IN_DIFF IN_SING;
2996     ¬(G,E same_side t)     []
2997     proof
2998       assume G,E same_side t     [Gsim_tE] by fol;
2999       A ∉ Open (G, E)     [notGAE] by fol t_line - SameSide_DEF ∉;
3000       G ∈ ray A E ━ {A}     [] by fol Distinct GnotAB notGAE IN_Ray GnotAB IN_DIFF IN_SING;
3001       ray A G = ray A E     [rAGrAE] by fol Distinct - RayWellDefined;
3002       ¬(C,G same_side t)     [Cnsim_tG] by fol t_line AGBncol Distinct Gsim_tE Cnsim_tE SameSideTransitive;
3003       C ∉ ray B G     [notCrBG] by fol - IN_Ray Distinct t_line AGBncol RaySameSide Cnsim_tG IN_DIFF IN_SING ∉;
3004       B ∈ Open (C, G)     [] by fol - GnotAB ∉ IN_Ray;
3005       ∡ G A B <_ang ∡ C B A     [] by fol AGBncol notCrBG - B1' EuclidPropositionI_16;
3006       ∡ E A B <_ang ∡ C B A     [] by fol - rAGrAE Angle_DEF;
3007       fol EABncol ANGLE AltIntAngCong - AngleTrichotomy1;
3008     qed;
3009     G,C same_side t     [Gsim_tC] by fol t_line AGBncol Distinct - Cnsim_tE AtMost2Sides;
3010     B ∉ Open (G, C)     [notGBC] by fol t_line - SameSide_DEF ∉;
3011     G ∈ ray B C ━ {B}     [] by fol Distinct GnotAB notGBC IN_Ray GnotAB IN_DIFF IN_SING;
3012     ray B G = ray B C     [rBGrBC] by fol Distinct - RayWellDefined;
3013     ∡ C B A ≡ ∡ E A B     [flipAltIntAngCong] by fol EABncol ANGLE AltIntAngCong C5Symmetric;
3014     ¬(E,G same_side t)     [Ensim_tG] by fol t_line AGBncol Distinct Gsim_tC Ensim_tC SameSideTransitive;
3015     E ∉ ray A G     [notErAG] by fol - IN_Ray Distinct t_line AGBncol RaySameSide Ensim_tG IN_DIFF IN_SING ∉;
3016     A ∈ Open (E, G)     [] by fol - GnotAB ∉ IN_Ray;
3017     ∡ G B A <_ang ∡ E A B     [] by fol AGBncol notErAG - B1' EuclidPropositionI_16;
3018     ∡ C B A <_ang ∡ E A B     [] by fol - rBGrBC Angle_DEF;
3019     fol EABncol ANGLE flipAltIntAngCong - AngleTrichotomy1;
3020   qed;
3021 `;;
3022
3023 let EuclidPropositionI_28 = theorem `;
3024   ∀A B C D E F G H l m t.  Line l ∧ A ∈ l ∧ B ∈ l ∧ G ∈ l  ⇒
3025     Line m ∧ C ∈ m ∧ D ∈ m ∧ H ∈ m  ⇒
3026     Line t ∧ G ∈ t ∧ H ∈ t  ⇒
3027     G ∉ m ∧ H ∉ l  ⇒
3028     G ∈ Open (A, B)  ∧ H ∈ Open (C, D)  ⇒
3029     G ∈ Open (E, H)  ∧  H ∈ Open (F, G)  ⇒
3030     ¬(D,A same_side t)  ⇒
3031     ∡ E G B ≡ ∡ G H D  ∨  ∡ B G H suppl ∡ G H D
3032     ⇒  l ∥ m
3033
3034   proof
3035     intro_TAC ∀A B C D E F G H l m t, l_line, m_line, t_line, notGmHl, H1, H2, H3, H4;
3036     ¬(A = G) ∧ ¬(G = B) ∧ ¬(H = D) ∧ ¬(E = G) ∧ ¬(G = H) ∧ Collinear A G B ∧ Collinear E G H     [Distinct] by fol H1 H2 B1';
3037     ¬Collinear H G A ∧ ¬Collinear G H D ∧ A ∉ t ∧ D ∉ t     [HGAncol] by fol Distinct l_line m_line notGmHl NonCollinearRaa CollinearSymmetry Collinear_DEF t_line ∉;
3038     ¬Collinear B G H ∧ ¬Collinear A G E ∧ ¬Collinear E G B     [BGHncol] by fol - Distinct CollinearSymmetry NoncollinearityExtendsToLine;
3039     ∡ A G H ≡ ∡ D H G     []
3040     proof
3041       case_split EGBeqGHD | BGHeqGHD     by fol H4;
3042       suppose ∡ E G B ≡ ∡ G H D;
3043         ∡ E G B ≡ ∡ H G A  ∧
3044         Angle (∡ E G B)  ∧  Angle (∡ H G A)  ∧  Angle (∡ G H D)      [boo] by fol BGHncol H1 H2 VerticalAnglesCong HGAncol ANGLE;
3045         ∡ H G A ≡ ∡ E G B     [] by fol - C5Symmetric;
3046         ∡ H G A ≡ ∡ G H D     [] by fol boo - EGBeqGHD C5Transitive;
3047         fol - AngleSymmetry;
3048       end;
3049       suppose ∡ B G H suppl ∡ G H D;
3050         ∡ B G H suppl ∡ H G A     [] by fol BGHncol H1 B1' SupplementaryAngles_DEF;
3051         fol - BGHeqGHD AngleSymmetry SupplementUnique AngleSymmetry;
3052       end;
3053     qed;
3054     fol l_line m_line t_line Distinct HGAncol H3 -  AlternateInteriorAngles;
3055   qed;
3056 `;;
3057
3058 let OppositeSidesCongImpliesParallelogram = theorem `;
3059   ∀A B C D.  Quadrilateral A B C D  ⇒
3060     seg A B ≡ seg C D  ∧  seg B C ≡ seg D A
3061     ⇒  Parallelogram A B C D
3062
3063   proof
3064     intro_TAC ∀A B C D, H1, H2;
3065     ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D) ∧
3066     ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B     [TetraABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF;
3067     consider a c such that
3068     Line a ∧ A ∈ a ∧ B ∈ a   ∧
3069     Line c ∧ C ∈ c ∧ D ∈ c     [ac_line] by fol TetraABCD I1;
3070     consider b d such that
3071     Line b ∧ B ∈ b ∧ C ∈ b   ∧
3072     Line d ∧ D ∈ d ∧ A ∈ d     [bd_line] by fol TetraABCD I1;
3073     consider l such that
3074     Line l ∧ A ∈ l ∧ C ∈ l     [l_line] by fol TetraABCD I1;
3075     consider m such that
3076     Line m ∧ B ∈ m ∧ D ∈ m     [m_line] by fol TetraABCD I1;
3077     B ∉ l ∧ D ∉ l ∧ A ∉ m  ∧ C ∉ m     [notBDlACm] by fol l_line m_line TetraABCD Collinear_DEF ∉;
3078     seg A C ≡ seg C A  ∧  seg B D ≡ seg D B     [seg_refl] by fol TetraABCD SEGMENT C2Reflexive SegmentSymmetry;
3079     A,B,C ≅ C,D,A     [] by fol TetraABCD H2 - SSS;
3080     ∡ B C A ≡ ∡ D A C  ∧  ∡ C A B ≡ ∡ A C D     [BCAeqDAC] by fol - TriangleCong_DEF;
3081     seg C D ≡ seg A B     [CDeqAB] by fol TetraABCD SEGMENT H2 C2Symmetric;
3082     B,C,D ≅ D,A,B     [] by fol TetraABCD H2 - seg_refl SSS;
3083     ∡ C D B ≡ ∡ A B D  ∧  ∡ D B C ≡ ∡ B D A  ∧  ∡ C B D ≡ ∡ A D B     [CDBeqABD] by fol - TriangleCong_DEF AngleSymmetry;
3084     ¬(B,D same_side l)  ∨  ¬(A,C same_side m)     [] by fol H1 l_line m_line FiveChoicesQuadrilateral;
3085     case_split Case1 | Ansim_mC     by fol -;
3086     suppose ¬(B,D same_side l);
3087       ¬(D,B same_side l)     [] by fol l_line notBDlACm - SameSideSymmetric;
3088       a ∥ c  ∧  b ∥ d     [] by fol ac_line l_line TetraABCD notBDlACm - BCAeqDAC AngleSymmetry AlternateInteriorAngles bd_line BCAeqDAC;
3089       fol H1 ac_line bd_line - Parallelogram_DEF;
3090     end;
3091     suppose ¬(A,C same_side m);
3092       b ∥ d     [b∥d] by fol bd_line m_line TetraABCD notBDlACm - CDBeqABD  AlternateInteriorAngles;
3093       c ∥ a     [] by fol ac_line m_line TetraABCD notBDlACm Ansim_mC CDBeqABD AlternateInteriorAngles;
3094       fol H1 ac_line bd_line b∥d - ParallelSymmetry Parallelogram_DEF;
3095     end;
3096   qed;
3097 `;;
3098
3099 let OppositeAnglesCongImpliesParallelogramHelp = theorem `;
3100   ∀A B C D a c.  Quadrilateral A B C D  ⇒
3101     ∡ A B C ≡ ∡ C D A  ∧  ∡ D A B ≡ ∡ B C D  ⇒
3102     Line a ∧ A ∈ a ∧ B ∈ a  ⇒  Line c  ∧ C ∈ c ∧ D ∈ c
3103     ⇒  a ∥ c
3104
3105   proof
3106     intro_TAC ∀A B C D a c, H1, H2, a_line, c_line;
3107     ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D) ∧
3108     ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B     [TetraABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF;
3109     ∡ C D A ≡ ∡ A B C  ∧  ∡ B C D ≡ ∡ D A B     [H2'] by fol TetraABCD ANGLE H2 C5Symmetric;
3110     consider l m such that
3111     Line l ∧ A ∈ l ∧ C ∈ l  ∧
3112     Line m ∧ B ∈ m ∧ D ∈ m     [lm_line] by fol TetraABCD I1;
3113     consider b d such that
3114     Line b ∧ B ∈ b ∧ C ∈ b   ∧  Line d ∧ D ∈ d ∧ A ∈ d     [bd_line] by fol TetraABCD I1;
3115     A ∉ c ∧ B ∉ c ∧ A ∉ b ∧ D ∉ b ∧ B ∉ d ∧ C ∉ d     [point_off_line] by fol c_line bd_line Collinear_DEF TetraABCD ∉;
3116     ¬(A ∈ int_triangle B C D  ∨  B ∈ int_triangle C D A  ∨
3117     C ∈ int_triangle D A B  ∨  D ∈ int_triangle A B C)     []
3118     proof
3119       assume A ∈ int_triangle B C D  ∨  B ∈ int_triangle C D A  ∨
3120       C ∈ int_triangle D A B  ∨  D ∈ int_triangle A B C     [Con] by fol;
3121       ∡ B C D <_ang ∡ D A B  ∨  ∡ C D A <_ang ∡ A B C  ∨
3122       ∡ D A B <_ang ∡ B C D  ∨  ∡ A B C <_ang ∡ C D A     [] by fol TetraABCD - EuclidPropositionI_21;
3123       fol - H2' H2 AngleTrichotomy1;
3124     qed;
3125     ConvexQuadrilateral A B C D     [] by fol H1 lm_line - FiveChoicesQuadrilateral;
3126     A ∈ int_angle B C D  ∧  B ∈ int_angle C D A  ∧
3127     C ∈ int_angle D A B  ∧  D ∈ int_angle A B C     [AintBCD] by fol - ConvexQuad_DEF;
3128     B,A same_side c  ∧  B,C same_side d     [Bsim_cA] by fol c_line bd_line - InteriorUse;
3129     A,D same_side b     [Asim_bD] by fol bd_line c_line AintBCD InteriorUse;
3130     assume ¬(a ∥ c)     [Con] by fol;
3131     consider G such that
3132     G ∈ a ∧ G ∈ c     [Gac] by fol - a_line c_line PARALLEL MEMBER_NOT_EMPTY IN_INTER;
3133     Collinear A B G ∧ Collinear D G C ∧ Collinear C G D     [ABGcol] by fol a_line - Collinear_DEF c_line;
3134     ¬(G = A) ∧ ¬(G = B) ∧ ¬(G = C) ∧ ¬(G = D)     [GnotABCD] by fol Gac ABGcol TetraABCD CollinearSymmetry Collinear_DEF;
3135     ¬Collinear B G C ∧ ¬Collinear A D G     [BGCncol] by fol c_line Gac GnotABCD point_off_line NonCollinearRaa CollinearSymmetry;
3136     ¬Collinear B C G ∧ ¬Collinear G B C ∧ ¬Collinear G A D ∧ ¬Collinear A G D     [BCGncol] by fol - CollinearSymmetry;
3137     G ∉ b ∧ G ∉ d     [notGb] by fol bd_line Collinear_DEF BGCncol ∉;
3138     G ∉ Open (B, A)     [notBGA] by fol Bsim_cA Gac SameSide_DEF ∉;
3139     B ∉ Open (A, G)     [notABG]
3140     proof
3141       assume ¬(B ∉ Open (A, G))     [Con] by fol;
3142       B ∈ Open (A, G)     [ABG] by fol - ∉;
3143       ray A B = ray A G     [rABrAG] by fol - IntervalRay;
3144       ¬(A,G same_side b)     [] by fol bd_line ABG SameSide_DEF;
3145       ¬(D,G same_side b)     [] by fol bd_line point_off_line notGb Asim_bD - SameSideTransitive;
3146       D ∉ ray C G     [] by fol bd_line notGb - RaySameSide TetraABCD IN_DIFF IN_SING ∉;
3147       C ∈ Open (D, G)     [DCG] by fol GnotABCD ABGcol - IN_Ray ∉;
3148       consider M such that
3149       D ∈ Open (C, M)     [CDM] by fol TetraABCD B2';
3150       D ∈ Open (G, M)     [GDM] by fol - B1' DCG TransitivityBetweennessHelp;
3151       ∡ C D A suppl ∡ A D M  ∧  ∡ A B C suppl ∡ C B G     [] by fol TetraABCD CDM ABG SupplementaryAngles_DEF;
3152       ∡ M D A ≡ ∡ G B C     [MDAeqGBC] by fol - H2' SupplementsCongAnglesCong AngleSymmetry;
3153       ∡ G A D <_ang ∡ M D A  ∧  ∡ G B C <_ang ∡ D C B     [] by fol BCGncol BGCncol GDM DCG B1' EuclidPropositionI_16;
3154       ∡ G A D <_ang ∡ D C B     [] by fol  - BCGncol ANGLE MDAeqGBC AngleTrichotomy2 AngleOrderTransitivity;
3155       ∡ D A B <_ang ∡ B C D     [] by fol - rABrAG Angle_DEF AngleSymmetry;
3156       fol - H2 AngleTrichotomy1;
3157     qed;
3158     A ∉ Open (G, B)     []
3159     proof
3160       assume ¬(A ∉ Open (G, B))     [Con] by fol;
3161       A ∈ Open (B, G)     [BAG] by fol - B1' ∉;
3162       ray B A = ray B G     [rBArBG] by fol - IntervalRay;
3163       ¬(B,G same_side d)     [] by fol bd_line BAG SameSide_DEF;
3164       ¬(C,G same_side d)     [] by fol bd_line point_off_line notGb Bsim_cA -  SameSideTransitive;
3165       C ∉ ray D G     [] by fol bd_line notGb - RaySameSide TetraABCD IN_DIFF IN_SING ∉;
3166       D ∈ Open (C, G)     [CDG] by fol GnotABCD ABGcol - IN_Ray ∉;
3167       consider M such that
3168       C ∈ Open (D, M)     [DCM] by fol B2' TetraABCD;
3169       C ∈ Open (G, M)     [GCM] by fol - B1' CDG TransitivityBetweennessHelp;
3170       ∡ B C D suppl ∡ M C B  ∧  ∡ D A B suppl ∡ G A D     [] by fol TetraABCD CollinearSymmetry DCM BAG SupplementaryAngles_DEF AngleSymmetry;
3171       ∡ M C B ≡ ∡ G A D     [GADeqMCB] by fol - H2' SupplementsCongAnglesCong;
3172       ∡ G B C <_ang ∡ M C B  ∧  ∡ G A D <_ang ∡ C D A     [] by fol BGCncol GCM BCGncol CDG B1' EuclidPropositionI_16;
3173       ∡ G B C <_ang ∡ C D A     [] by fol - BCGncol ANGLE GADeqMCB AngleTrichotomy2 AngleOrderTransitivity;
3174       ∡ A B C <_ang ∡ C D A     [] by fol - rBArBG Angle_DEF;
3175       fol - H2 AngleTrichotomy1;
3176     qed;
3177     fol TetraABCD GnotABCD ABGcol notABG notBGA - B3' ∉;
3178   qed;
3179 `;;
3180
3181 let OppositeAnglesCongImpliesParallelogram = theorem `;
3182   ∀A B C D. Quadrilateral A B C D  ⇒
3183     ∡ A B C ≡ ∡ C D A  ∧  ∡ D A B ≡ ∡ B C D
3184     ⇒  Parallelogram A B C D
3185
3186   proof
3187     intro_TAC ∀A B C D, H1, H2;
3188     Quadrilateral B C D A     [QuadBCDA] by fol H1 QuadrilateralSymmetry;
3189     ¬(A = B) ∧ ¬(B = C) ∧ ¬(C = D) ∧ ¬(D = A) ∧ ¬Collinear B C D ∧ ¬Collinear D A B     [TetraABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF;
3190     ∡ B C D ≡ ∡ D A B     [H2'] by fol TetraABCD ANGLE H2 C5Symmetric;
3191     consider a such that
3192     Line a ∧ A ∈ a ∧ B ∈ a     [a_line] by fol TetraABCD I1;
3193     consider b such that
3194     Line b ∧ B ∈ b ∧ C ∈ b     [b_line] by fol TetraABCD I1;
3195     consider c such that
3196     Line c  ∧ C ∈ c ∧ D ∈ c     [c_line] by fol TetraABCD I1;
3197     consider d such that
3198     Line d ∧ D ∈ d ∧ A ∈ d     [d_line] by fol TetraABCD I1;
3199     fol H1 QuadBCDA H2 H2' a_line b_line c_line d_line OppositeAnglesCongImpliesParallelogramHelp Parallelogram_DEF;
3200   qed;
3201 `;;
3202
3203 let P = NewAxiom
3204   `;∀P l. Line l ∧ P ∉ l  ⇒ ∃! m. Line m ∧ P ∈ m ∧ m ∥ l`;;
3205
3206 NewConstant("μ",`:(point->bool)->real`);;
3207
3208 let AMa = NewAxiom
3209  `;∀α. Angle α  ⇒  &0 < μ α ∧ μ α < &180`;;
3210
3211 let AMb = NewAxiom
3212  `;∀α. Right α  ⇒  μ α  = &90`;;
3213
3214 let AMc = NewAxiom
3215  `;∀α β. Angle α ∧ Angle β ∧ α ≡ β  ⇒  μ α = μ β`;;
3216
3217 let AMd = NewAxiom
3218  `;∀A O B P. P ∈ int_angle A O B  ⇒  μ (∡ A O B) = μ (∡ A O P) + μ (∡ P O B)`;;
3219
3220 let ConverseAlternateInteriorAngles = theorem `;
3221   ∀A B C E l m.  Line l ∧ A ∈ l ∧ E ∈ l  ⇒
3222     Line m ∧ B ∈ m ∧ C ∈ m  ⇒ Line t ∧ A ∈ t ∧ B ∈ t  ⇒
3223     ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t  ⇒
3224     ¬(C,E same_side t)  ⇒  l ∥ m
3225     ⇒  ∡ E A B ≡ ∡ C B A
3226
3227   proof
3228     intro_TAC ∀A B C E l m, l_line, m_line, t_line, Distinct, Cnsim_tE, para_lm;
3229     ¬Collinear C B A     [] by fol Distinct t_line NonCollinearRaa CollinearSymmetry;
3230     A ∉ m ∧ Angle (∡ C B A)     [notAm] by fol m_line - Collinear_DEF ∉ ANGLE;
3231     consider D such that
3232     ¬(A = D) ∧ D ∉ t ∧ ¬(C,D same_side t) ∧ seg A D ≡ seg A E  ∧  ∡ B A D ≡ ∡ C B A     [Dexists] by simplify C4OppositeSide -  Distinct t_line;
3233     consider k such that
3234     Line k ∧ A ∈ k ∧ D ∈ k     [k_line] by fol Distinct I1;
3235     k ∥ m     [] by fol - m_line t_line Dexists Distinct AngleSymmetry AlternateInteriorAngles;
3236     k = l     [] by fol m_line notAm l_line k_line - para_lm P;
3237     D,E same_side t  ∧  A ∉ Open (D, E)  ∧  Collinear A E D     [] by fol t_line Distinct Dexists Cnsim_tE AtMost2Sides SameSide_DEF ∉ - k_line l_line Collinear_DEF;
3238     ray A D = ray A E     [] by fol Distinct - IN_Ray Dexists RayWellDefined IN_DIFF IN_SING;
3239     fol - Dexists AngleSymmetry Angle_DEF;
3240   qed;
3241 `;;
3242
3243 let HilbertTriangleSum = theorem `;
3244   ∀A B C.  ¬Collinear A B C
3245     ⇒  ∃E F. B ∈ Open (E, F)  ∧  C ∈ int_angle A B F  ∧
3246            ∡ E B A ≡ ∡ C A B  ∧  ∡ C B F ≡ ∡ B C A
3247
3248   proof
3249     intro_TAC ∀A B C, ABCncol;
3250     ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear C A B     [Distinct] by fol ABCncol NonCollinearImpliesDistinct CollinearSymmetry;
3251     consider l such that
3252     Line l ∧ A ∈ l ∧ C ∈ l     [l_line] by fol Distinct I1;
3253     consider x such that
3254     Line x ∧ A ∈ x ∧ B ∈ x     [x_line] by fol Distinct I1;
3255     consider y such that
3256     Line y ∧ B ∈ y ∧ C ∈ y     [y_line] by fol Distinct I1;
3257     C ∉ x     [notCx] by fol x_line ABCncol Collinear_DEF ∉;
3258     Angle (∡ C A B)     [] by fol ABCncol CollinearSymmetry ANGLE;
3259     consider E such that
3260     ¬(B = E) ∧ E ∉ x ∧ ¬(C,E same_side x) ∧ seg B E ≡ seg A B ∧ ∡ A B E ≡ ∡ C A B     [Eexists] by simplify C4OppositeSide - Distinct x_line notCx;
3261     consider m such that
3262     Line m ∧ B ∈ m ∧ E ∈ m     [m_line] by fol - I1;
3263     ∡ E B A ≡ ∡ C A B     [EBAeqCAB] by fol Eexists AngleSymmetry;
3264     m ∥ l     [para_lm] by fol m_line l_line x_line Eexists Distinct notCx - AlternateInteriorAngles;
3265     m ∩ l = ∅     [ml0] by fol - PARALLEL;
3266     C ∉ m ∧ A ∉ m     [notACm] by fol - l_line INTER_COMM DisjointOneNotOther;
3267     consider F such that
3268     B ∈ Open (E, F)     [EBF] by fol Eexists B2';
3269     ¬(B = F) ∧ F ∈ m     [EBF'] by fol - B1' m_line BetweenLinear;
3270     ¬Collinear A B F ∧ F ∉ x      [ABFncol] by fol EBF' m_line notACm NonCollinearRaa CollinearSymmetry Collinear_DEF x_line ∉;
3271     ¬(E,F same_side x) ∧ ¬(E,F same_side y)     [Ensim_yF] by fol EBF x_line y_line SameSide_DEF;
3272     C,F same_side x     [Csim_xF] by fol x_line notCx Eexists ABFncol Eexists - AtMost2Sides;
3273     C,A same_side m     [] by fol m_line l_line ml0 DisjointLinesImplySameSide;
3274     C ∈ int_angle A B F     [CintABF] by fol ABFncol x_line m_line EBF' notCx notACm Csim_xF - IN_InteriorAngle;
3275     A ∈ int_angle C B E     [] by fol EBF B1' - InteriorAngleSymmetry InteriorReflectionInterior;
3276     A ∉ y  ∧  A,E same_side y     [Asim_yE] by fol y_line m_line - InteriorUse;
3277     E ∉ y ∧ F ∉ y     [notEFy] by fol y_line m_line EBF' Eexists EBF' I1 Collinear_DEF notACm ∉;
3278     E,A same_side y     [] by fol y_line - Asim_yE SameSideSymmetric;
3279     ¬(A,F same_side y)     [Ansim_yF] by fol y_line notEFy Asim_yE - Ensim_yF SameSideTransitive;
3280     ∡ F B C ≡ ∡ A C B     [] by fol m_line EBF' l_line y_line EBF' Distinct notEFy Asim_yE Ansim_yF para_lm ConverseAlternateInteriorAngles;
3281     fol EBF CintABF EBAeqCAB - AngleSymmetry;
3282   qed;
3283 `;;
3284
3285 let EuclidPropositionI_13 = theorem `;
3286   ∀A O B A'.  ¬Collinear A O B  ∧  O ∈ Open (A, A')
3287     ⇒  μ (∡ A O B) + μ (∡ B O A') = &180
3288
3289   proof
3290     intro_TAC ∀A O B A', H1 H2;
3291     case_split RightAOB | notRightAOB     by fol -;
3292     suppose Right (∡ A O B);
3293       Right (∡ B O A')  ∧  μ (∡ A O B) = &90  ∧  μ (∡ B O A') = &90     [] by fol H1 H2 - RightImpliesSupplRight AMb;
3294       real_arithmetic -;
3295     end;
3296     suppose ¬Right (∡ A O B);
3297       ¬(A = O) ∧ ¬(O = B)     [Distinct] by fol H1 NonCollinearImpliesDistinct;
3298       consider l such that
3299       Line l ∧ O ∈ l ∧ A ∈ l ∧ A' ∈ l     [l_line] by fol - I1 H2 BetweenLinear;
3300       B ∉ l     [notBl] by fol - Distinct I1 Collinear_DEF H1 ∉;
3301       consider F such that
3302       Right (∡ O A F)  ∧  Angle (∡ O A F)     [RightOAF] by fol Distinct EuclidPropositionI_11 RightImpliesAngle;
3303       ∃! r. Ray r ∧ ∃E. ¬(O = E) ∧ r = ray O E ∧ E ∉ l ∧ E,B same_side l ∧ ∡ A O E ≡ ∡ O A F     [] by simplify C4 - Distinct l_line notBl;
3304       consider E such that
3305       ¬(O = E)  ∧  E ∉ l  ∧  E,B same_side l  ∧  ∡ A O E ≡ ∡ O A F     [Eexists] by fol -;
3306       ¬Collinear A O E     [AOEncol] by fol Distinct l_line - NonCollinearRaa CollinearSymmetry;
3307       Right (∡ A O E)     [RightAOE] by fol - ANGLE RightOAF Eexists CongRightImpliesRight;
3308       Right (∡ E O A')  ∧  μ (∡ A O E) = &90  ∧  μ (∡ E O A') = &90     [RightEOA'] by fol AOEncol H2 -  RightImpliesSupplRight AMb;
3309       ¬(∡ A O B ≡ ∡ A O E)     [] by fol notRightAOB H1 ANGLE RightAOE CongRightImpliesRight;
3310       ¬(∡ A O B = ∡ A O E)     [] by fol H1 AOEncol ANGLE - C5Reflexive;
3311       ¬(ray O B = ray O E)     [] by fol - Angle_DEF;
3312       B ∉ ray O E  ∧  O ∉ Open (B, E)     [] by fol Distinct - Eexists RayWellDefined IN_DIFF IN_SING ∉ l_line B1' SameSide_DEF;
3313       ¬Collinear O E B     [] by fol - Eexists IN_Ray ∉;
3314       E ∈ int_angle A O B  ∨  B ∈ int_angle A O E     [] by fol Distinct l_line Eexists notBl AngleOrdering - CollinearSymmetry InteriorAngleSymmetry;
3315       case_split EintAOB | BintAOE     by fol -;
3316       suppose E ∈ int_angle A O B;
3317         B ∈ int_angle E O A'     [] by fol H2 - InteriorReflectionInterior;
3318         μ (∡ A O B) = μ (∡ A O E) + μ (∡ E O B)  ∧
3319         μ (∡ E O A') = μ (∡ E O B) + μ (∡ B O A')     [] by fol EintAOB - AMd;
3320         real_arithmetic - RightEOA';
3321       end;
3322       suppose B ∈ int_angle A O E;
3323         E ∈ int_angle B O A'     [] by fol H2 - InteriorReflectionInterior;
3324         μ (∡ A O E) = μ (∡ A O B) + μ (∡ B O E)  ∧
3325         μ (∡ B O A') = μ (∡ B O E) + μ (∡ E O A')     [] by fol BintAOE - AMd;
3326         real_arithmetic - RightEOA';
3327       end;
3328     end;
3329   qed;
3330 `;;
3331
3332 let TriangleSum = theorem `;
3333   ∀A B C. ¬Collinear A B C
3334     ⇒  μ (∡ A B C) + μ (∡ B C A) + μ (∡ C A B) = &180
3335
3336   proof
3337     intro_TAC ∀A B C, ABCncol;
3338     ¬Collinear C A B  ∧  ¬Collinear B C A     [CABncol] by fol ABCncol CollinearSymmetry;
3339     consider E F such that
3340     B ∈ Open (E, F)  ∧  C ∈ int_angle A B F  ∧  ∡ E B A ≡ ∡ C A B  ∧  ∡ C B F ≡ ∡ B C A     [EBF] by fol ABCncol HilbertTriangleSum;
3341     ¬Collinear C B F  ∧  ¬Collinear A B F  ∧  Collinear E B F  ∧  ¬(B = E)     [CBFncol] by fol - InteriorAngleSymmetry InteriorEZHelp IN_InteriorAngle B1' CollinearSymmetry;
3342     ¬Collinear E B A     [EBAncol] by fol CollinearSymmetry - NoncollinearityExtendsToLine;
3343     μ (∡ A B F) = μ (∡ A B C) + μ (∡ C B F)     [μCintABF] by fol EBF AMd;
3344     μ (∡ E B A) + μ (∡ A B F) = &180     [suppl180] by fol EBAncol EBF EuclidPropositionI_13;
3345     μ (∡ C A B) = μ (∡ E B A)  ∧  μ (∡ B C A) = μ (∡ C B F)     [] by fol CABncol EBAncol CBFncol ANGLE EBF AMc;
3346     real_arithmetic suppl180 μCintABF -;
3347   qed;
3348 `;;
3349
3350 let CircleConvex2_THM = theorem `;
3351   ∀O A B C. ¬Collinear A O B  ⇒  B ∈ Open (A, C)  ⇒
3352     seg O A <__ seg O B  ∨  seg O A ≡ seg O B
3353     ⇒  seg O B <__ seg O C
3354
3355   proof
3356     intro_TAC ∀O A B C, H1, H2, H3;
3357     ¬Collinear O B A ∧ ¬Collinear B O A ∧ ¬Collinear O A B ∧ ¬(O = A) ∧ ¬(O = B)     [H1'] by fol H1 CollinearSymmetry NonCollinearImpliesDistinct;
3358     B ∈ Open (C, A) ∧ ¬(C = A) ∧ ¬(C = B) ∧ Collinear A B C ∧ Collinear B A C     [H2'] by fol H2 B1' CollinearSymmetry;
3359     ¬Collinear O B C ∧ ¬Collinear O C B     [OBCncol] by fol H1' - NoncollinearityExtendsToLine CollinearSymmetry;
3360     ¬Collinear O A C     [OABncol] by fol H1' H2' NoncollinearityExtendsToLine;
3361     ∡ O C B <_ang ∡ O B A     [OCBlessOBA] by fol OBCncol H2' ExteriorAngle;
3362     ∡ O A B <_ang ∡ O B C     [OABlessOBC] by fol H1' H2 ExteriorAngle;
3363     ∡ O B A <_ang ∡ B A O  ∨  ∡ O B A ≡ ∡ B A O     []
3364     proof
3365       assume seg O A ≡ seg O B [Cong]     by fol H3 H1' EuclidPropositionI_18;
3366       seg O B ≡ seg O A     [] by fol H1' SEGMENT - C2Symmetric;
3367       fol H1' - IsoscelesCongBaseAngles AngleSymmetry;
3368     qed;
3369     ∡ O B A <_ang ∡ O A B  ∨  ∡ O B A ≡ ∡ O A B     [OBAlessOAB] by fol - AngleSymmetry;
3370     ∡ O C B <_ang ∡ O B C     [] by fol OCBlessOBA - OABlessOBC OBCncol H1' OABncol OBCncol ANGLE - AngleOrderTransitivity AngleTrichotomy2;
3371     fol OBCncol - AngleSymmetry EuclidPropositionI_19;
3372   qed;
3373 `;;