RichterHilbertAxiomGeometry/miz3/FontHilbertAxiom.ml

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