---

Step * of Lemma geo-Aax4

∀g:EuclideanPlane. ∀a,b,c:Point. ∀l,m:Line.  (a ≠ b ⇒ (a I l ∧ b I l) ⇒ ((a I m ∧ c I m) ∧ c # l) ⇒ b # m)
BY
{ ((Auto THEN GetLinePoints (6) THEN GetLinePoints (5))
   THEN (Unfold `geo-plsep` 0 THEN Unfold `geo-plsep` -1)
   THEN All
   Reduce⋅) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x1 : Point
6. y1 : Point
7. l2 : x1 ≠ y1
8. x : Point
9. y : Point
10. m2 : x ≠ y
11. a ≠ b
12. a I <x1, y1, l2>
13. b I <x1, y1, l2>
14. a I <x, y, m2>
15. c I <x, y, m2>
16. c # x1y1
⊢ b # xy

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  GetLinePoints  (6)  THEN  GetLinePoints  (5))
  THEN  (Unfold  `geo-plsep`  0  THEN  Unfold  `geo-plsep`  -1)
  THEN  All
  Reduce\mcdot{})

---

Home Index