---

Step * of Lemma geo-parallel_functionality

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

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a' : Point
7. b' : Point
8. c' : Point
9. d' : Point
10. a ≡ a'
11. b ≡ b'
12. c ≡ c'
13. d ≡ d'
14. a ≠ b
15. c ≠ d
16. ∀x:Point. (Colinear(a;b;x) ⇒ x # cd)
17. x : Point
18. Colinear(a';b';x)
⊢ x # c'd'

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  D  -1  THEN  D  0)  THEN  Auto)

---

Home Index