---

Step * of Lemma geo-parallel-points-implies

∀e:EuclideanPlane. ∀a,b,x,y:Point.
  (geo-parallel-points(e;a;b;x;y)
  ⇒ (a ≠ b ∧ x ≠ y)
  ⇒ (∀x1,y1:{z:Point| Colinear(z;a;b)} .  (x1 leftof xy ⇒ (¬y1 leftof yx))))
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. geo-parallel-points(e;a;b;x;y)
7. a ≠ b
8. x ≠ y
9. x1 : {z:Point| Colinear(z;a;b)} 
10. y1 : {z:Point| Colinear(z;a;b)} 
11. x1 leftof xy
⊢ ¬y1 leftof yx

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y:Point.
    (geo-parallel-points(e;a;b;x;y)
    {}\mRightarrow{}  (a  \mneq{}  b  \mwedge{}  x  \mneq{}  y)
    {}\mRightarrow{}  (\mforall{}x1,y1:\{z:Point|  Colinear(z;a;b)\}  .    (x1  leftof  xy  {}\mRightarrow{}  (\mneg{}y1  leftof  yx))))


By

---

Latex:
Auto

---

Home Index