---

Step * of Lemma geo-Aax2

∀g:EuclideanPlane. ∀a,b:Point. ∀l,m:Line.  (a ≠ b ⇒ (a I l ∧ a I m) ⇒ (b I l ∧ b I m) ⇒ l ≡ m)
BY
{ (RWO "geo-incident-line" 0
   THEN Auto
   THEN GetLinePoints 5
   THEN GetLinePoints 4
   THEN (D 0 THENA Auto)
   THEN RepUR ``geo-line-sep`` -1
   THEN ExRepD) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. x1 : Point
5. y1 : Point
6. l2 : x1 ≠ y1
7. x : Point
8. y : Point
9. m2 : x ≠ y
10. a ≠ b
11. Colinear(a;x1;y1)
12. Colinear(a;x;y)
13. Colinear(b;x1;y1)
14. Colinear(b;x;y)
15. p : Point
16. Colinear(p;x1;y1)
17. p # xy
⊢ False

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}l,m:Line.    (a  \mneq{}  b  {}\mRightarrow{}  (a  I  l  \mwedge{}  a  I  m)  {}\mRightarrow{}  (b  I  l  \mwedge{}  b  I  m)  {}\mRightarrow{}  l  \mequiv{}  m)


By

---

Latex:
(RWO  "geo-incident-line"  0
  THEN  Auto
  THEN  GetLinePoints  5
  THEN  GetLinePoints  4
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``geo-line-sep``  -1
  THEN  ExRepD)

---

Home Index