---

Step * of Lemma geo-parallel-symmetry

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (geo-parallel(e;a;b;c;d) ⇒ geo-parallel(e;c;d;a;b))
BY
{ ((Auto THEN D 0 THEN Auto) THEN D 6) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b ∧ c ≠ d
7. ∀x:Point. (Colinear(a;b;x) ⇒ x # cd)
8. x : Point
9. Colinear(c;d;x)
⊢ x # ab

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (geo-parallel(e;a;b;c;d)  {}\mRightarrow{}  geo-parallel(e;c;d;a;b))


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)  THEN  D  6)

---

Home Index