RichterHilbertAxiomGeometry/thmFontHilbertAxiom.ml

   1 ocaml
   2 #use "hol.ml";;
   3 #load "unix.cma";;
   4 loadt "miz3/miz3.ml";;
   5
   6 reset_miz3 0;;
   7
   8 verbose := true;;
   9 report_timing := true;;
  10
  11 Theorem/Proof templates:
  12
  13 let  = theorem `;
  14
  15   proof
  16
  17   qed;
  18 `;;
  19
  20 interactive_goal `;
  21 `;;
  22 interactive_proof `;
  23 `;;
  24 interactive_proof `;
  25 `;;
  26 interactive_proof `;
  27 `;;
  28 interactive_proof `;
  29 `;;
  30 interactive_proof `;
  31 `;;
  32
  33 ∉     |- ∀ a l. a ∉ l ⇔ ¬(a ∈ l)
  34
  35 Interval_DEF     |- ∀ A B X. open (A,B) = {X | Between A X B}
  36
  37 Collinear_DEF
  38   |- ∀ A B C. Collinear A B C  ⇔  ∃ l. Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l
  39
  40 SameSide_DEF
  41   |- ∀ l A B. A,B same_side l  ⇔  Line l ∧ ¬ ∃ X. X ∈ l ∧ X ∈ open (A,B)
  42
  43 Ray_DEF     |- ∀ A B. ray A B =
  44                  {X | ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)}
  45
  46 Ordered_DEF
  47    |- ∀ A C B D.
  48         ordered A B C D  ⇔
  49         B ∈ open (A,C) ∧ B ∈ open (A,D) ∧ C ∈ open (A,D) ∧ C ∈ open (B,D)
  50
  51 InteriorAngle_DEF     |- ∀ A O B.
  52          int_angle A O B =
  53          {P | ¬Collinear A O B ∧
  54               ∃ a b.
  55                    Line a ∧ O ∈ a ∧ A ∈ a ∧
  56                    Line b ∧ O ∈ b ∧ B ∈ b ∧
  57                    P ∉ a ∧ P ∉ b ∧
  58                    P,B same_side a ∧ P,A same_side b}
  59
  60 InteriorTriangle_DEF
  61   |- ∀ A B C.
  62         int_triangle A B C =
  63          {P | P ∈ int_angle A B C  ∧
  64               P ∈ int_angle B C A  ∧
  65               P ∈ int_angle C A B}
  66
  67 Tetralateral_DEF
  68   |- ∀ C D A B.
  69        Tetralateral A B C D  ⇔
  70        ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D) ∧
  71        ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B
  72
  73 Quadrilateral_DEF
  74   |- ∀ B C D A.
  75          Quadrilateral A B C D  ⇔
  76          Tetralateral A B C D ∧
  77          open (A,B) ∩ open (C,D) = ∅ ∧
  78          open (B,C) ∩ open (D,A) = ∅
  79
  80 ConvexQuad_DEF
  81   |- ∀ D A B C.
  82          ConvexQuadrilateral A B C D ⇔
  83          Quadrilateral A B C D ∧
  84          A ∈ int_angle B C D ∧
  85          B ∈ int_angle C D A ∧
  86          C ∈ int_angle D A B ∧
  87          D ∈ int_angle A B C
  88
  89 Segment_DEF     |- ∀ A B. seg A B = {A, B} ∪ open (A,B)
  90
  91 SEGMENT     |- ∀ s. Segment s  ⇔  ∃ A B. s = seg A B ∧ ¬(A = B)
  92
  93 SegmentOrdering_DEF
  94   |- ∀ t s.
  95          s <__ t ⇔
  96          Segment s ∧
  97          ∃ C D X. t = seg C D  ∧  X ∈ open (C,D)  ∧  s ≡ seg C X
  98
  99 Angle_DEF     |- ∀ A O B. ∡ A O B = ray O A ∪ ray O B
 100
 101 ANGLE
 102   |- ∀ α. Angle α  ⇔  ∃ A O B. α = ∡ A O B ∧ ¬Collinear A O B
 103
 104 AngleOrdering_DEF
 105   |- ∀ β α.
 106          α <_ang β ⇔
 107          Angle α ∧
 108          ∃ A O B G.
 109               ¬Collinear A O B  ∧  β = ∡ A O B ∧
 110               G ∈ int_angle A O B  ∧  α ≡ ∡ A O G
 111
 112 RAY     |- ∀ r. Ray r ⇔ ∃ O A. ¬(O = A)  ∧  r = ray O A
 113
 114 TriangleCong_DEF
 115   |- ∀ A B C A' B' C'.
 116          A,B,C ≅ A',B',C' ⇔
 117          ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
 118          seg A B ≡ seg A' B' ∧
 119          seg A C ≡ seg A' C' ∧
 120          seg B C ≡ seg B' C' ∧
 121          ∡ A B C ≡ ∡ A' B' C' ∧
 122          ∡ B C A ≡ ∡ B' C' A' ∧
 123          ∡ C A B ≡ ∡ C' A' B'
 124
 125 SupplementaryAngles_DEF
 126   |- ∀α β.
 127          α suppl β ⇔
 128          ∃ A O B A'.
 129               ¬Collinear A O B ∧ O ∈ open (A,A') ∧
 130               α = ∡ A O B  ∧  β = ∡ B O A'
 131
 132 RightAngle_DEF
 133   |- ∀α. Right α ⇔ ∃ β. α suppl β ∧ α ≡ β
 134
 135 PlaneComplement_DEF
 136   |- ∀ α. complement α = {P | P ∉ α}
 137
 138 CONVEX
 139   |- ∀α. Convex α ⇔
 140              ∀ A B. A ∈ α ∧ B ∈ α ⇒ open (A,B) ⊂ α
 141
 142 PARALLEL
 143   |- ∀ l k. l ∥ k  ⇔  Line l  ∧  Line k  ∧  l ∩ k = ∅
 144
 145 Parallelogram_DEF
 146   |- ∀ A B C D.
 147          Parallelogram A B C D  ⇔
 148          Quadrilateral A B C D ∧
 149          ∃ a b c d.
 150               Line a ∧ A ∈ a ∧ B ∈ a ∧ Line b ∧ B ∈ b ∧ C ∈ b ∧
 151               Line c ∧ C ∈ c ∧ D ∈ d ∧ Line d ∧ D ∈ d ∧ A ∈ d ∧
 152               a ∥ c  ∧  b ∥ d
 153
 154 InteriorCircle_DEF
 155   |- ∀ O R. int_circle O R = {P | ¬(O = R) ∧ (P = O ∨ seg O P <__ seg O R)}
 156
 157
 158 I1     |- ∀ A B. ¬(A = B) ⇒ (∃! l. Line l ∧ A ∈ l ∧ B ∈ l)
 159
 160 I2     |- ∀ l. Line l ⇒ (∃ A B. A ∈ l ∧ B ∈ l ∧ ¬(A = B))
 161
 162 I3     |- ∃ A B C. ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear A B C
 163
 164 B1     |- ∀ A B C.
 165          Between A B C
 166          ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
 167              Between C B A ∧ Collinear A B C
 168
 169 B2     |- ∀ A B. ¬(A = B)  ⇒  ∃C. Between A B C
 170
 171 B3     |- ∀ A B C.
 172          ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
 173          ⇒ (Between A B C ∨ Between B C A ∨ Between C A B) ∧
 174              ¬(Between A B C ∧ Between B C A) ∧
 175              ¬(Between A B C ∧ Between C A B) ∧
 176              ¬(Between B C A ∧ Between C A B)
 177
 178 B4     |- ∀ l A B C.
 179          Line l ∧
 180          ¬Collinear A B C ∧
 181          A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
 182          (∃X. X ∈ l ∧ Between A X C)
 183          ⇒ (∃ Y. Y ∈ l ∧ Between A Y B) ∨
 184              (∃ Y. Y ∈ l ∧ Between B Y C)
 185
 186 C1     |- ∀ s O Z.
 187          Segment s ∧ ¬(O = Z)
 188          ⇒ ∃! P. P ∈ ray O Z ━ O  ∧  seg O P ≡ s
 189
 190 C2Reflexive     |- Segment s ⇒ s ≡ s
 191
 192 C2Symmetric     |- Segment s ∧ Segment t ∧ s ≡ t ⇒ t ≡ s
 193
 194 C2Transitive
 195   |- Segment s ∧ Segment t ∧ Segment u ∧ s ≡ t ∧ t ≡ u ⇒ s ≡ u
 196
 197 C3     |- ∀ A B C A' B' C'.
 198          B ∈ open (A,C) ∧ B' ∈ open (A',C') ∧
 199          seg A B ≡ seg A' B' ∧ seg B C ≡ seg B' C'
 200          ⇒ seg A C ≡ seg A' C'
 201
 202 C4     |- ∀ α O A l Y.
 203          Angle α ∧ ¬(O = A) ∧ Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l
 204          ⇒  ∃! r. Ray r ∧ ∃ B. ¬(O = B) ∧ r = ray O B ∧
 205                     B ∉ l  ∧ B,Y same_side l ∧ ∡ A O B ≡ α
 206
 207 C5Reflexive     |- Angle α ⇒ α ≡ α
 208
 209 C5Symmetric
 210   |- Angle α ∧ Angle β ∧ α ≡ β ⇒ β ≡ α
 211
 212 C5Transitive
 213   |- Angle α ∧ Angle β ∧ Angle γ ∧ α ≡ β ∧ β ≡ γ
 214      ⇒ α ≡ γ
 215
 216 C6     |- ∀A B C A' B' C'.
 217          ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
 218          seg B A ≡ seg B' A' ∧ seg B C ≡ seg B' C' ∧
 219          ∡ A B C ≡ ∡ A' B' C'
 220          ⇒ ∡ B C A ≡ ∡ B' C' A'
 221
 222
 223 IN_Interval     |- ∀ A B X. X ∈ open (A,B) ⇔ Between A X B
 224
 225 IN_Ray     |- ∀ A B X.
 226          X ∈ ray A B  ⇔  ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)
 227
 228 IN_InteriorAngle     |- ∀A O B P.
 229          P ∈ int_angle A O B  ⇔  ¬Collinear A O B ∧  ∃ a b.
 230          Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
 231          P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b
 232
 233 IN_InteriorTriangle
 234   |- ∀A B C P.
 235          P ∈ int_triangle A B C ⇔
 236          P ∈ int_angle A B C ∧ P ∈ int_angle B C A ∧ P ∈ int_angle C A B
 237
 238 IN_PlaneComplement
 239   |- ∀α P. P ∈ complement α ⇔ P ∉ α
 240
 241 IN_InteriorCircle
 242   |- ∀ O R P.
 243          P ∈ int_circle O R ⇔ ¬(O = R) ∧ (P = O ∨ seg O P <__ seg O R)
 244
 245 B1'     |- ∀ A B C.
 246          B ∈ open (A,C)
 247          ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
 248              B ∈ open (C,A) ∧ Collinear A B C
 249
 250 B2'     |- ∀ A B. ¬(A = B) ⇒ (∃ C. B ∈ open (A,C))
 251
 252 B3'     |- ∀ A B C.
 253          ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
 254          ⇒ (B ∈ open (A,C) ∨ C ∈ open (B,A) ∨ A ∈ open (C,B)) ∧
 255              ¬(B ∈ open (A,C) ∧ C ∈ open (B,A)) ∧
 256              ¬(B ∈ open (A,C) ∧ A ∈ open (C,B)) ∧
 257              ¬(C ∈ open (B,A) ∧ A ∈ open (C,B))
 258
 259 B4'     |- ∀ l A B C.
 260          Line l  ∧  ¬Collinear A B C  ∧  A ∉ l  ∧  B ∉ l  ∧  C ∉ l  ∧
 261          (∃ X. X ∈ l ∧ X ∈ open (A,C))
 262          ⇒ (∃ Y. Y ∈ l ∧ Y ∈ open (A,B)) ∨
 263            (∃ Y. Y ∈ l ∧ Y ∈ open (B,C))
 264
 265 B4''     |- ∀ l A B C.
 266          Line l  ∧  ¬Collinear A B C  ∧  A ∉ l  ∧  B ∉ l  ∧  C ∉ l  ∧
 267          A,B same_side l  ∧  B,C same_side l
 268          ⇒ A,C same_side l
 269
 270 DisjointOneNotOther
 271   |- ∀ l m. (∀x. x ∈ m ⇒ x ∉ l)  ⇔  l ∩ m = ∅
 272
 273 EquivIntersectionHelp
 274   |- ∀ e x l m.
 275          (l ∩ m = {x} ∨ m ∩ l = {x})  ∧  e ∈ m ━ x  ⇒  e ∉ l
 276
 277 CollinearSymmetry
 278   |- ∀ A B C.
 279          Collinear A B C
 280          ⇒ Collinear A C B ∧ Collinear B A C ∧
 281              Collinear B C A ∧ Collinear C A B ∧ Collinear C B A
 282
 283 ExistsNewPointOnLine
 284   |- ∀ P l. Line l ∧ P ∈ l  ⇒  ∃ Q. Q ∈ l ∧ ¬(P = Q)
 285
 286 ExistsPointOffLine     |- ∀ l. Line l ⇒ ∃ Q. Q ∉ l
 287
 288 BetweenLinear
 289   |- ∀ A B C m.
 290          Line m ∧ A ∈ m ∧ C ∈ m ∧
 291          B ∈ open (A,C) ∨ C ∈ open (B,A) ∨ A ∈ open (C,B)
 292          ⇒ B ∈ m
 293
 294 CollinearLinear
 295   |- ∀ A B C m.
 296          Line m ∧ A ∈ m ∧ C ∈ m ∧ ¬(A = C) ∧
 297          Collinear A B C ∨ Collinear B C A ∨ Collinear C A B
 298          ⇒ B ∈ m
 299
 300 NonCollinearImpliesDistinct
 301   |- ∀ A B C. ¬Collinear A B C ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)
 302
 303 NonCollinearRaa
 304   |- ∀A B C l.
 305          ¬(A = C)  ∧  Line l ∧ A ∈ l ∧ C ∈ l  ∧  B ∉ l
 306          ⇒ ¬Collinear A B C
 307
 308 TwoSidesTriangle1Intersection
 309   |- ∀A B C Y.
 310          ¬Collinear A B C ∧ Collinear B C Y ∧ Collinear A C Y  ⇒  Y = C
 311
 312 OriginInRay     |- ∀ O Q. ¬(Q = O) ⇒ O ∈ ray O Q
 313
 314 EndpointInRay     |- ∀ O Q. ¬(Q = O) ⇒ Q ∈ ray O Q
 315
 316 I1Uniqueness
 317   |- ∀ X l m.
 318          Line l ∧ Line m ∧ ¬(l = m) ∧ X ∈ l ∧ X ∈ m
 319          ⇒ l ∩ m = {X}
 320
 321 EquivIntersection
 322   |- ∀ A B X l m.
 323          Line l  ∧  Line m  ∧  l ∩ m = {X}  ∧
 324          A ∈ m ━ X  ∧  B ∈ m ━ X  ∧  X ∉ open (A,B)
 325          ⇒ A,B same_side l
 326
 327 RayLine
 328   |- ∀ O P l. Line l ∧ O ∈ l ∧ P ∈ l ⇒ ray O P ⊂ l
 329
 330 RaySameSide
 331   |- ∀ l O A P.
 332          Line l  ∧  O ∈ l  ∧  A ∉ l  ∧  P ∈ ray O A ━ O
 333          ⇒ P ∉ l ∧ P,A same_side l
 334
 335 IntervalRayEZ
 336   |- ∀ A B C.
 337          B ∈ open (A,C)  ⇒  B ∈ ray A C ━ A  ∧  C ∈ ray A B ━ A
 338
 339 NoncollinearityExtendsToLine
 340   |- ∀ A O B X.
 341          ¬Collinear A O B  ∧  Collinear O B X  ∧  ¬(X = O)
 342          ⇒ ¬Collinear A O X
 343
 344 SameSideReflexive
 345   |- ∀ l A. Line l ∧ A ∉ l ⇒ A,A same_side l
 346
 347 SameSideSymmetric
 348   |- ∀ l A B.
 349          Line l ∧ A ∉ l ∧ B ∉ l  ∧  A,B same_side l
 350          ⇒ B,A same_side l
 351
 352 SameSideTransitive
 353   |- ∀l A B C.
 354          Line l ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l  ∧
 355          A,B same_side l ∧ B,C same_side l
 356          ⇒ A,C same_side l
 357
 358 ConverseCrossbar
 359   |- ∀ O A B G. ¬Collinear A O B  ∧  G ∈ open (A,B)  ⇒  G ∈ int_angle A O B
 360
 361 InteriorUse
 362   |- ∀ A O B P a b.
 363          Line a ∧ O ∈ a ∧ A ∈ a  ∧
 364          Line b ∧ O ∈ b ∧ B ∈ b  ∧
 365          P ∈ int_angle A O B
 366          ⇒ P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b
 367
 368 InteriorEZHelp
 369   |- ∀ A O B P.
 370          P ∈ int_angle A O B
 371          ⇒ ¬(P = A) ∧ ¬(P = O) ∧ ¬(P = B) ∧ ¬Collinear A O P
 372
 373 InteriorAngleSymmetry
 374   |- ∀ A O B P. P ∈ int_angle A O B  ⇒  P ∈ int_angle B O A
 375
 376 InteriorWellDefined
 377   |- ∀ A O B X P.
 378          P ∈ int_angle A O B  ∧  X ∈ ray O B ━ O  ⇒  P ∈ int_angle A O X
 379
 380 WholeRayInterior
 381   |- ∀A O B X P.
 382          X ∈ int_angle A O B  ∧  P ∈ ray O X ━ O
 383          ⇒ P ∈ int_angle A O B
 384
 385 AngleOrdering
 386   |- ∀ O A P Q a.
 387          ¬(O = A) ∧ Line a ∧ O ∈ a ∧ A ∈ a ∧ P ∉ a ∧ Q ∉ a ∧
 388          P,Q same_side a  ∧  ¬Collinear P O Q
 389          ⇒ P ∈ int_angle Q O A  ∨  Q ∈ int_angle P O A
 390
 391 InteriorsDisjointSupplement
 392   |- ∀A O B A'.
 393          ¬Collinear A O B  ∧  O ∈ open (A,A')
 394          ⇒ int_angle A O B ∩ int_angle B O A' = ∅
 395
 396 InteriorReflectionInterior
 397   |- ∀ A O B D A'.
 398          O ∈ open (A,A')  ∧  D ∈ int_angle A O B  ⇒  B ∈ int_angle D O A'
 399
 400 Crossbar_THM
 401   |- ∀ O A B D.
 402          D ∈ int_angle A O B
 403          ⇒ ∃ G. G ∈ open (A,B) ∧ G ∈ ray O D ━ O
 404
 405 AlternateConverseCrossbar
 406   |- ∀ O A B G. Collinear A G B  ∧  G ∈ int_angle A O B  ⇒  G ∈ open (A,B)
 407
 408 InteriorOpposite
 409   |- ∀ A O B P p.
 410          P ∈ int_angle A O B  ∧  Line p ∧ O ∈ p ∧ P ∈ p
 411          ⇒ ¬(A,B same_side p)
 412
 413 IntervalTransitivity
 414   |- ∀ O P Q R m.
 415          Line m  ∧ O ∈ m  ∧
 416          P ∈ m ━ O  ∧  Q ∈ m ━ O  ∧  R ∈ m ━ O  ∧
 417          O ∉ open (P,Q)  ∧  O ∉ open (Q,R)
 418          ⇒ O ∉ open (P,R)
 419
 420 RayWellDefinedHalfway
 421   |- ∀ O P Q. ¬(Q = O)  ∧  P ∈ ray O Q ━ O  ⇒  ray O P ⊂ ray O Q
 422
 423 RayWellDefined
 424   |- ∀ O P Q. ¬(Q = O)  ∧  P ∈ ray O Q ━ O  ⇒  ray O P = ray O Q
 425
 426 OppositeRaysIntersect1pointHelp
 427   |- ∀ A O B X.
 428          O ∈ open (A,B)  ∧  X ∈ ray O B ━ O
 429          ⇒ X ∉ ray O A  ∧  O ∈ open (X,A)
 430
 431 OppositeRaysIntersect1point
 432   |- ∀ A O B. O ∈ open (A,B)  ⇒  ray O A ∩ ray O B = {O}
 433
 434 IntervalRay
 435   |- ∀ A B C. B ∈ open (A,C)  ⇒  ray A B = ray A C
 436
 437 Reverse4Order
 438   |- ∀ A B C D. ordered A B C D ⇒ ordered D C B A
 439
 440 TransitivityBetweennessHelp
 441   |- ∀ A B C D. B ∈ open (A,C) ∧ C ∈ open (B,D)  ⇒  B ∈ open (A,D)
 442
 443 TransitivityBetweenness
 444   |- ∀ A B C D. B ∈ open (A,C) ∧ C ∈ open (B,D)  ⇒  ordered A B C D
 445
 446 IntervalsAreConvex
 447   |- ∀ A B C. B ∈ open (A,C) ⇒ open (A,B) ⊂ open (A,C)
 448
 449 TransitivityBetweennessVariant
 450   |- ∀ A X B C. X ∈ open (A,B) ∧ B ∈ open (A,C)  ⇒  ordered A X B C
 451
 452 Interval2sides2aLineHelp
 453   |- ∀ A B C X. B ∈ open (A,C)  ⇒  X ∉ open (A,B) ∨ X ∉ open (B,C)
 454
 455 Interval2sides2aLine
 456   |- ∀ A B C X.
 457          Collinear A B C
 458          ⇒ X ∉ open (A,B) ∨ X ∉ open (A,C) ∨ X ∉ open (B,C)
 459
 460 TwosidesTriangle2aLine
 461   |- ∀A B C Y l m.
 462          Line l ∧ ¬Collinear A B C ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l  ∧
 463          Line m ∧ A ∈ m ∧ C ∈ m  ∧
 464          Y ∈ l ∧ Y ∈ m  ∧ ¬(A,B same_side l) ∧ ¬(B,C same_side l)
 465          ⇒ A,C same_side l
 466
 467 LineUnionOf2Rays
 468   |- ∀ A O B l.
 469          Line l ∧ A ∈ l ∧ B ∈ l  ∧  O ∈ open (A,B)
 470          ⇒ l = ray O A ∪ ray O B
 471
 472 AtMost2Sides
 473   |- ∀ A B C l.
 474          Line l ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l
 475          ⇒ A,B same_side l ∨ A,C same_side l ∨ B,C same_side l
 476
 477 FourPointsOrder
 478   |- ∀ A B C X l.
 479      Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ X ∈ l  ∧  B ∈ open (A,C)  ∧
 480      ¬(X = A) ∧ ¬(X = B) ∧ ¬(X = C)
 481      ⇒ ordered X A B C ∨ ordered A X B C ∨ ordered A B X C ∨ ordered A B C X
 482
 483 HilbertAxiomRedundantByMoore
 484   |- ∀ A B C D l.
 485          Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ D ∈ l  ∧
 486          ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D)
 487          ⇒ ordered D A B C ∨ ordered A D B C ∨ ordered A B D C ∨
 488             ordered A B C D ∨ ordered D A C B ∨ ordered A D C B ∨
 489             ordered A C D B ∨ ordered A C B D ∨ ordered D C A B ∨
 490             ordered C D A B ∨ ordered C A D B ∨ ordered C A B D
 491
 492 InteriorTransitivity
 493   |- ∀A O B F G.
 494          G ∈ int_angle A O B  ∧  F ∈ int_angle A O G
 495          ⇒ F ∈ int_angle A O B
 496
 497 HalfPlaneConvexNonempty
 498   |- ∀l H A.
 499          Line l  ∧  A ∉ l  ∧  H = {X | X ∉ l ∧ X,A same_side l}
 500          ⇒ ¬(H = ∅)  ∧  H ⊂ complement l  ∧  Convex H
 501
 502 PlaneSeparation
 503   |- ∀ l. Line l
 504          ⇒ ∃ H1 H2.
 505                H1 ∩ H2 = ∅  ∧  ¬(H1 = ∅)  ∧  ¬(H2 = ∅) ∧
 506                Convex H1  ∧  Convex H2  ∧  complement l = H1 ∪ H2 ∧
 507                ∀ P Q. P ∈ H1 ∧ Q ∈ H2  ⇒  ¬(P,Q same_side l)
 508
 509 TetralateralSymmetry
 510   |- ∀ A B C D.
 511          Tetralateral A B C D
 512          ⇒ Tetralateral B C D A ∧ Tetralateral A B D C
 513
 514 EasyEmptyIntersectionsTetralateralHelp
 515   |- ∀ A B C D. Tetralateral A B C D  ⇒  open (A,B) ∩ open (B,C) = ∅
 516
 517 EasyEmptyIntersectionsTetralateral
 518   |- ∀ A B C D.
 519        Tetralateral A B C D
 520        ⇒ open (A,B) ∩ open (B,C) = ∅  ∧  open (B,C) ∩ open (C,D) = ∅  ∧
 521           open (C,D) ∩ open (D,A) = ∅  ∧  open (D,A) ∩ open (A,B) = ∅
 522
 523 SegmentSameSideOppositeLine
 524   |- ∀ A B C D a c.
 525          Quadrilateral A B C D  ∧
 526          Line a ∧ A ∈ a ∧ B ∈ a  ∧  Line c ∧ C ∈ c ∧ D ∈ c
 527          ⇒ A,B same_side c  ∨  C,D same_side a
 528
 529 ConvexImpliesQuad
 530   |- ∀ A B C D.
 531          Tetralateral A B C D  ∧
 532          C ∈ int_angle D A B  ∧  D ∈ int_angle A B C
 533          ⇒ Quadrilateral A B C D
 534
 535 DiagonalsIntersectImpliesConvexQuad
 536   |- ∀ A B C D G.
 537          ¬Collinear B C D  ∧  G ∈ open (A,C)  ∧  G ∈ open (B,D)
 538          ⇒ ConvexQuadrilateral A B C D
 539
 540 DoubleNotSimImpliesDiagonalsIntersect
 541   |- ∀ A B C D l m.
 542          Line l ∧ A ∈ l ∧ C ∈ l  ∧
 543          Line m ∧ B ∈ m ∧ D ∈ m  ∧
 544          Tetralateral A B C D  ∧
 545          ¬(B,D same_side l)  ∧  ¬(A,C same_side m)
 546          ⇒ (∃ G. G ∈ open (A,C) ∩ open (B,D)) ∧
 547              ConvexQuadrilateral A B C D
 548
 549 ConvexQuadImpliesDiagonalsIntersect
 550   |- ∀ A B C D l m.
 551          Line l ∧ A ∈ l ∧ C ∈ l  ∧
 552          Line m ∧ B ∈ m ∧ D ∈ m  ∧
 553          ConvexQuadrilateral A B C D
 554          ⇒ ¬(B,D same_side l) ∧ ¬(A,C same_side m) ∧
 555              (∃ G. G ∈ open (A,C) ∩ open (B,D)) ∧
 556              ¬Quadrilateral A B D C
 557
 558 FourChoicesTetralateralHelp
 559   |- ∀ A B C D.
 560          Tetralateral A B C D  ∧  C ∈ int_angle D A B
 561          ⇒ ConvexQuadrilateral A B C D  ∨  C ∈ int_triangle D A B
 562
 563 InteriorTriangleSymmetry
 564   |- ∀ A B C P. P ∈ int_triangle A B C  ⇒  P ∈ int_triangle B C A
 565
 566 FourChoicesTetralateral
 567   |- ∀ A B C D a.
 568          Tetralateral A B C D  ∧  Line a ∧ A ∈ a ∧ B ∈ a  ∧
 569          C,D same_side a
 570          ⇒ ConvexQuadrilateral A B C D  ∨  ConvexQuadrilateral A B D C  ∨
 571             D ∈ int_triangle A B C  ∨  C ∈ int_triangle D A B
 572
 573 QuadrilateralSymmetry
 574   |- ∀ A B C D.
 575          Quadrilateral A B C D
 576          ⇒ Quadrilateral B C D A ∧
 577              Quadrilateral C D A B ∧
 578              Quadrilateral D A B C
 579
 580 FiveChoicesQuadrilateral
 581   |- ∀ A B C D l m.
 582          Quadrilateral A B C D  ∧
 583          Line l ∧ A ∈ l ∧ C ∈ l  ∧
 584          Line m ∧ B ∈ m ∧ D ∈ m
 585          ⇒ (ConvexQuadrilateral A B C D  ∨
 586               A ∈ int_triangle B C D  ∨  B ∈ int_triangle C D A   ∨
 587               C ∈ int_triangle D A B  ∨  D ∈ int_triangle A B C)  ∧
 588             (¬(B,D same_side l) ∨ ¬(A,C same_side m))
 589
 590 IntervalSymmetry     |- ∀ A B. open (A,B) = open (B,A)
 591
 592 SegmentSymmetry     |- ∀ A B. seg A B = seg B A
 593
 594 C1OppositeRay
 595   |- ∀ O P s.
 596          Segment s ∧ ¬(O = P)  ⇒  ∃ Q. P ∈ open (O,Q) ∧ seg P Q ≡ s
 597
 598 OrderedCongruentSegments
 599   |- ∀ A B C D F.
 600          ¬(A = C) ∧ ¬(D = F)  ∧  seg A C ≡ seg D F  ∧  B ∈ open (A,C)
 601          ⇒ ∃ E. E ∈ open (D,F)  ∧  seg A B ≡ seg D E
 602
 603 SegmentSubtraction
 604   |- ∀ A B C A' B' C'.
 605          B ∈ open (A,C) ∧ B' ∈ open (A',C')  ∧
 606          seg A B ≡ seg A' B'  ∧  seg A C ≡ seg A' C'
 607          ⇒ seg B C ≡ seg B' C'
 608
 609 SegmentOrderingUse
 610   |- ∀A B s.
 611          Segment s  ∧  ¬(A = B)  ∧  s <__ seg A B
 612          ⇒ ∃ G. G ∈ open (A,B) ∧ s ≡ seg A G
 613
 614 SegmentTrichotomy1     |- ∀ s t. s <__ t  ⇒  ¬(s ≡ t)
 615
 616 SegmentTrichotomy2
 617   |- ∀ s t u. s <__ t ∧ Segment u ∧ t ≡ u  ⇒  s <__ u
 618
 619 SegmentOrderTransitivity
 620   |- ∀ s t u. s <__ t ∧ t <__ u  ⇒  s <__ u
 621
 622 SegmentTrichotomy
 623   |- ∀ s t.
 624        Segment s ∧ Segment t
 625        ⇒ (s ≡ t  ∨  s <__ t  ∨  t <__ s) ∧
 626           ¬(s ≡ t ∧ s <__ t) ∧ ¬(s ≡ t ∧ t <__ s) ∧ ¬(s <__ t ∧ t <__ s)
 627
 628 C4Uniqueness
 629   |- ∀ O A B P l.
 630          Line l ∧ O ∈ l ∧ A ∈ l ∧ ¬(O = A)  ∧
 631          B ∉ l ∧ P ∉ l ∧ P,B same_side l  ∧  ∡ A O P ≡ ∡ A O B
 632          ⇒ ray O B = ray O P
 633
 634 AngleSymmetry     |- ∀ A O B. ∡ A O B = ∡ B O A
 635
 636 TriangleCongSymmetry
 637   |- ∀ A B C A' B' C'.
 638          A,B,C ≅ A',B',C'
 639          ⇒ A,C,B ≅ A',C',B'  ∧  B,A,C ≅ B',A',C'  ∧
 640             B,C,A ≅ B',C',A'  ∧  C,A,B ≅ C',A',B'  ∧  C,B,A ≅ C',B',A'
 641
 642 SAS
 643   |- ∀ A B C A' B' C'.
 644          ¬Collinear A B C ∧ ¬Collinear A' B' C'    ∧
 645          seg B A ≡ seg B' A'  ∧  seg B C ≡ seg B' C'  ∧
 646          ∡ A B C ≡ ∡ A' B' C'
 647          ⇒ A,B,C ≅ A',B',C'
 648
 649 ASA
 650   |- ∀ A B C A' B' C'.
 651          ¬Collinear A B C  ∧  ¬Collinear A' B' C'  ∧
 652          seg A C ≡ seg A' C'  ∧
 653          ∡ C A B ≡ ∡ C' A' B'  ∧  ∡ B C A ≡ ∡ B' C' A'
 654          ⇒ A,B,C ≅ A',B',C'
 655
 656 AngleSubtraction
 657   |- ∀ A O B A' O' B' G G'.
 658          G ∈ int_angle A O B  ∧  G' ∈ int_angle A' O' B'  ∧
 659          ∡ A O B ≡ ∡ A' O' B'  ∧  ∡ A O G ≡ ∡ A' O' G'
 660          ⇒ ∡ G O B ≡ ∡ G' O' B'
 661
 662 OrderedCongruentAngles
 663   |- ∀ A O B A' O' B' G.
 664          ¬Collinear A' O' B'  ∧ ∡ A O B ≡ ∡ A' O' B'  ∧
 665          G ∈ int_angle A O B
 666          ⇒ ∃ G'. G' ∈ int_angle A' O' B'  ∧  ∡ A O G ≡ ∡ A' O' G'
 667
 668 AngleAddition
 669   |- ∀ A O B A' O' B' G G'.
 670          G ∈ int_angle A O B  ∧  G' ∈ int_angle A' O' B'  ∧
 671          ∡ A O G ≡ ∡ A' O' G'  ∧  ∡ G O B ≡ ∡ G' O' B'  ∧
 672          ⇒ ∡ A O B ≡ ∡ A' O' B'
 673
 674 AngleOrderingUse
 675   |- ∀ A O B α.
 676          Angle α  ∧  ¬Collinear A O B  ∧  α <_ang ∡ A O B
 677          ⇒ (∃ G. G ∈ int_angle A O B ∧ α ≡ ∡ A O G)
 678
 679 AngleTrichotomy1
 680   |- ∀ α β. α <_ang β ⇒ ¬(α ≡ β)
 681
 682 AngleTrichotomy2
 683   |- ∀ α β γ.
 684          α <_ang β  ∧  Angle γ  ∧  β ≡ γ
 685          ⇒ α <_ang γ
 686
 687 AngleOrderTransitivity
 688   |- ∀α β γ.
 689          α <_ang β  ∧  β <_ang γ
 690          ⇒ α <_ang γ
 691
 692 AngleTrichotomy
 693   |- ∀ α β.
 694          Angle α ∧ Angle β
 695          ⇒ (α ≡ β ∨ α <_ang β ∨ β <_ang α) ∧
 696              ¬(α ≡ β ∧ α <_ang β) ∧
 697              ¬(α ≡ β ∧ β <_ang α) ∧
 698              ¬(α <_ang β ∧ β <_ang α)
 699
 700 SupplementExists
 701   |- ∀ α. Angle α  ⇒  ∃ α'. α suppl α'
 702
 703 SupplementImpliesAngle
 704   |- ∀ α β. α suppl β  ⇒  Angle α ∧ Angle β
 705
 706 RightImpliesAngle     |- ∀ α. Right α  ⇒  Angle α
 707
 708 SupplementSymmetry
 709   |- ∀ α β. α suppl β  ⇒  β suppl α
 710
 711 SupplementsCongAnglesCong
 712   |- ∀ α β α' β'.
 713          α suppl α'  ∧  β suppl β'  ∧  α ≡ β
 714          ⇒ α' ≡ β'
 715
 716 SupplementUnique
 717   |- ∀ α β β'.
 718          α suppl β  ∧  α suppl β'  ⇒  β ≡ β'
 719
 720 CongRightImpliesRight
 721   |- ∀ α β.
 722          Angle α ∧ Right β ∧ α ≡ β  ⇒  Right α
 723
 724 RightAnglesCongruentHelp
 725   |- ∀ A O B A' P a.
 726          ¬Collinear A O B  ∧  O ∈ open (A,A')
 727          Right (∡ A O B)  ∧  Right (∡ A O P)
 728          ⇒ P ∉ int_angle A O B
 729
 730 RightAnglesCongruent
 731   |- ∀ α β. Right α ∧ Right β  ⇒  α ≡ β
 732
 733 OppositeRightAnglesLinear
 734   |- ∀ A B O H h.
 735          ¬Collinear A O H ∧ ¬Collinear H O B  ∧
 736          Right (∡ A O H) ∧ Right (∡ H O B)  ∧
 737          Line h ∧ O ∈ h ∧ H ∈ h  ∧ ¬(A,B same_side h)
 738          ⇒ O ∈ open (A,B)
 739
 740 RightImpliesSupplRight
 741   |- ∀ A O B A'.
 742          ¬Collinear A O B  ∧  O ∈ open (A,A')  ∧  Right (∡ A O B)
 743          ⇒ Right (∡ B O A')
 744
 745 IsoscelesCongBaseAngles
 746   |- ∀ A B C.
 747          ¬Collinear A B C  ∧  seg B A ≡ seg B C
 748          ⇒ ∡ C A B ≡ ∡ A C B
 749
 750 C4withC1
 751   |- ∀ α l O A Y P Q.
 752          Angle α ∧ ¬(O = A) ∧ ¬(P = Q)  ∧
 753          Line l ∧ O ∈ l ∧ A ∈ l  ∧  Y ∉ l
 754          ⇒ ∃ N. ¬(O = N) ∧ N ∉ l  ∧  N,Y same_side l  ∧
 755                   seg O N ≡ seg P Q  ∧  ∡ A O N ≡ α
 756
 757 C4OppositeSide
 758   |- ∀ α l O A Z P Q.
 759          Angle α ∧ ¬(O = A) ∧ ¬(P = Q)  ∧
 760          Line l ∧ O ∈ l ∧ A ∈ l ∧ Z ∉ l
 761          ⇒ ∃ N. ¬(O = N) ∧ N ∉ l ∧ ¬(Z,N same_side l) ∧
 762                  seg O N ≡ seg P Q  ∧  ∡ A O N ≡ α
 763
 764 SSS
 765   |- ∀ A B C A' B' C'.
 766      ¬Collinear A B C  ∧  ¬Collinear A' B' C'  ∧
 767      seg A B ≡ seg A' B'  ∧  seg A C ≡ seg A' C'  ∧  seg B C ≡ seg B' C'
 768      ⇒ A,B,C ≅ A',B',C'
 769
 770 AngleBisector
 771   |- ∀ A B C.
 772          ¬Collinear B A C
 773          ⇒ ∃ F. F ∈ int_angle B A C  ∧  ∡ B A F ≡ ∡ F A C
 774
 775 EuclidPropositionI_6
 776   |- ∀ A B C.
 777          ¬Collinear A B C  ∧  ∡ B A C ≡ ∡ B C A
 778          ⇒ seg B A ≡ seg B C
 779
 780 IsoscelesExists
 781   |- ∀ A B. ¬(A = B)  ⇒  ∃ D. ¬Collinear A D B  ∧  seg D A ≡ seg D B
 782
 783 MidpointExists
 784   |- ∀ A B. ¬(A = B)  ⇒  ∃ M. M ∈ open (A,B) ∧ seg A M ≡ seg M B
 785
 786 EuclidPropositionI_7short
 787   |- ∀ A B C D a.
 788          ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a ∧ ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧
 789          C,D same_side a  ∧  seg A C ≡ seg A D
 790          ⇒ ¬(seg B C ≡ seg B D)
 791
 792 EuclidPropI_7Help
 793   |- ∀ A B C D a.
 794          ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a ∧ ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧
 795          C,D same_side a  ∧  seg A C ≡ seg A D  ∧
 796          (C ∈ int_triangle D A B  ∨  ConvexQuadrilateral A B C D)
 797          ⇒ ¬(seg B C ≡ seg B D)
 798
 799 EuclidPropositionI_7
 800   |- ∀ A B C D a.
 801          ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a ∧ ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧
 802          C,D same_side a  ∧  seg A C ≡ seg A D
 803          ⇒ ¬(seg B C ≡ seg B D)
 804
 805 EuclidPropositionI_11
 806   |- ∀A B. ¬(A = B) ⇒  ∃ F. Right (∡ A B F)
 807
 808 DropPerpendicularToLine
 809   |- ∀ P l.
 810          Line l  ∧  P ∉ l
 811          ⇒ ∃ E Q. E ∈ l ∧ Q ∈ l ∧ Right (∡ P Q E)
 812
 813 EuclidPropositionI_14
 814   |- ∀ A B C D l.
 815          Line l ∧ A ∈ l ∧ B ∈ l ∧ ¬(A = B) ∧
 816          C ∉ l ∧ D ∉ l  ∧  ¬(C,D same_side l) ∧
 817          ∡ C B A suppl ∡ A B D
 818          ⇒ B ∈ open (C,D)
 819
 820 VerticalAnglesCong
 821   |- ∀ A B O A' B'.
 822          ¬Collinear A O B ∧ O ∈ open (A,A') ∧ O ∈ open (B,B')
 823          ⇒ ∡ B O A' ≡ ∡ B' O A
 824
 825 EuclidPropositionI_16
 826   |- ∀ A B C D.
 827          ¬Collinear A B C  ∧  C ∈ open (B,D)
 828          ⇒ ∡ B A C <_ang ∡ D C A
 829
 830 ExteriorAngle
 831   |- ∀ A B C D.
 832          ¬Collinear A B C  ∧  C ∈ open (B,D)
 833          ⇒ ∡ A B C <_ang ∡ A C D
 834
 835 EuclidPropositionI_17
 836   |- ∀ A B C α β γ.
 837        ¬Collinear A B C  ∧  α = ∡ A B C  ∧  β = ∡ B C A  ∧  β suppl γ
 838        ⇒ α <_ang γ
 839
 840 EuclidPropositionI_18
 841   |- ∀ A B C.
 842          ¬Collinear A B C  ∧  seg A C <__ seg A B
 843          ⇒ ∡ A B C <_ang ∡ B C A
 844
 845 EuclidPropositionI_19
 846   |- ∀ A B C.
 847          ¬Collinear A B C  ∧  ∡ A B C <_ang ∡ B C A
 848          ⇒ seg A C <__ seg A B
 849
 850 EuclidPropositionI_20
 851   |- ∀ A B C D.
 852          ¬Collinear A B C  ∧  A ∈ open (B,D)  ∧  seg A D ≡ seg A C
 853          ⇒ seg B C <__ seg B D
 854
 855 EuclidPropositionI_21
 856   |- ∀ A B C D.
 857          ¬Collinear A B C  ∧  D ∈ int_triangle A B C
 858          ⇒ ∡ A B C <_ang ∡ C D A
 859
 860 AngleTrichotomy3
 861   |- ∀ α β γ.
 862          α <_ang β  ∧  Angle γ  ∧  γ ≡ α
 863          ⇒ γ <_ang β
 864
 865 InteriorCircleConvexHelp
 866   |- ∀ O A B C.
 867          ¬Collinear A O C  ∧  B ∈ open (A,C)  ∧
 868          seg O A <__ seg O C  ∨  seg O A ≡ seg O C
 869          ⇒ seg O B <__ seg O C
 870
 871 InteriorCircleConvex
 872   |- ∀ O R A B C.
 873          ¬(O = R)  ∧  B ∈ open (A,C)  ∧
 874          A ∈ int_circle O R  ∧  C ∈ int_circle O R
 875          ⇒ B ∈ int_circle O R
 876
 877 SegmentTrichotomy3
 878   |- ∀ s t u. s <__ t  ∧  Segment u  ∧  u ≡ s  ⇒  u <__ t
 879
 880 EuclidPropositionI_24Help
 881   |- ∀ O A C O' D F.
 882          ¬Collinear A O C ∧ ¬Collinear D O' F  ∧
 883          seg O' D ≡ seg O A  ∧  seg O' F ≡ seg O C  ∧
 884          ∡ D O' F <_ang ∡ A O C  ∧
 885          seg O A <__ seg O C  ∨  seg O A ≡ seg O C
 886          ⇒ seg D F <__ seg A C
 887
 888 EuclidPropositionI_24
 889   |- ∀ O A C O' D F.
 890          ¬Collinear A O C ∧ ¬Collinear D O' F  ∧
 891          seg O' D ≡ seg O A  ∧  seg O' F ≡ seg O C  ∧
 892          ∡ D O' F <_ang ∡ A O C
 893          ⇒ seg D F <__ seg A C
 894
 895 EuclidPropositionI_25
 896   |- ∀ O A C O' D F.
 897          ¬Collinear A O C ∧ ¬Collinear D O' F  ∧
 898          seg O' D ≡ seg O A  ∧  seg O' F ≡ seg O C  ∧
 899          seg D F <__ seg A C
 900          ⇒ ∡ D O' F <_ang ∡ A O C
 901
 902 AAS
 903   |- ∀ A B C A' B' C'.
 904          ¬Collinear A B C ∧ ¬Collinear A' B' C'  ∧
 905          ∡ A B C ≡ ∡ A' B' C'  ∧  ∡ B C A ≡ ∡ B' C' A'  ∧
 906          seg A B ≡ seg A' B'
 907          ⇒ A,B,C ≅ A',B',C'
 908
 909 ParallelSymmetry     |- ∀ l k. l ∥ k  ⇒  k ∥ l
 910
 911 AlternateInteriorAngles
 912   |- ∀ A B C E l m t.
 913          Line l ∧ A ∈ l ∧ E ∈ l ∧
 914          Line m ∧ B ∈ m ∧ C ∈ m ∧
 915          Line t ∧ A ∈ t ∧ B ∈ t ∧
 916          ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t ∧
 917          ¬(C,E same_side t)  ∧  ∡ E A B ≡ ∡ C B A
 918          ⇒ l ∥ m
 919
 920 EuclidPropositionI_28
 921   |- ∀ A B C D E F G H l m t.
 922          Line l ∧ A ∈ l ∧ B ∈ l ∧ G ∈ l ∧
 923          Line m ∧ C ∈ m ∧ D ∈ m ∧ H ∈ m ∧
 924          Line t ∧ G ∈ t ∧ H ∈ t ∧ G ∉ m ∧ H ∉ l ∧
 925          G ∈ open (A,B)  ∧  H ∈ open (C,D)  ∧
 926          G ∈ open (E,H)  ∧  H ∈ open (F,G)  ∧  ¬(D,A same_side t)  ∧
 927          ∡ E G B ≡ ∡ G H D  ∨  ∡ B G H suppl ∡ G H D
 928          ⇒ l ∥ m
 929
 930 OppositeSidesCongImpliesParallelogram
 931   |- ∀ A B C D.
 932          Quadrilateral A B C D  ∧
 933          seg A B ≡ seg C D  ∧  seg B C ≡ seg D A
 934          ⇒ Parallelogram A B C D
 935
 936 OppositeAnglesCongImpliesParallelogramHelp
 937   |- ∀ A B C D a c.
 938          Quadrilateral A B C D                                ∧
 939          ∡ A B C ≡ ∡ C D A  ∧  ∡ D A B ≡ ∡ B C D             ∧
 940          Line a ∧ A ∈ a ∧ B ∈ a  ∧  Line c ∧ C ∈ c ∧ D ∈ c
 941          ⇒ a ∥ c
 942
 943 OppositeAnglesCongImpliesParallelogram
 944   |- ∀ A B C D.
 945          Quadrilateral A B C D  ∧
 946          ∡ A B C ≡ ∡ C D A  ∧  ∡ D A B ≡ ∡ B C D
 947          ⇒ Parallelogram A B C D
 948
 949
 950 P     |- ∀ P l. Line l ∧ P ∉ l ⇒ ∃! m. Line m ∧ P ∈ m ∧ m ∥ l
 951
 952 AMa     |- ∀ α. Angle α ⇒ &0 < μ α ∧ μ α < &180
 953
 954 AMb     |- ∀ α. Right α ⇒ μ α = &90
 955
 956 AMc     |- ∀ α β. Angle α ∧ Angle β ∧ α ≡ β ⇒ μ α = μ β
 957
 958 AMd     |- ∀ A O B P. P ∈ int_angle A O B
 959          ⇒ μ (∡ A O B) = μ (∡ A O P) + μ (∡ P O B)
 960
 961
 962 ConverseAlternateInteriorAngles
 963   |- ∀ A B C E l m t.
 964          Line l ∧ A ∈ l ∧ E ∈ l                         ∧
 965          Line m ∧ B ∈ m ∧ C ∈ m                         ∧
 966          Line t ∧ A ∈ t ∧ B ∈ t                         ∧
 967          ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t ∧
 968          ¬(C,E same_side t)  ∧  l ∥ m
 969          ⇒ ∡ E A B ≡ ∡ C B A
 970
 971 HilbertTriangleSum
 972   |- ∀ A B C.
 973          ¬Collinear A B C
 974          ⇒ ∃ E F.
 975                   B ∈ open (E,F)  ∧  C ∈ int_angle A B F ∧
 976                   ∡ E B A ≡ ∡ C A B  ∧  ∡ C B F ≡ ∡ B C A
 977
 978 EuclidPropositionI_13
 979   |- ∀A O B A'.
 980          ¬Collinear A O B  ∧  O ∈ open (A,A')
 981          ⇒ μ (∡ A O B) + μ (∡ B O A') = &180
 982
 983 TriangleSum
 984   |- ∀ A B C.
 985          ¬Collinear A B C
 986          ⇒ μ (∡ A B C) + μ (∡ B C A) + μ (∡ C A B) = &180