---

Step * 1 of Lemma geo-parallel_functionality


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'
BY
{ (RWO "10< 11<" (-1) 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:

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  \mequiv{}  a'
11.  b  \mequiv{}  b'
12.  c  \mequiv{}  c'
13.  d  \mequiv{}  d'
14.  a  \mneq{}  b
15.  c  \mneq{}  d
16.  \mforall{}x:Point.  (Colinear(a;b;x)  {}\mRightarrow{}  x  \#  cd)
17.  x  :  Point
18.  Colinear(a';b';x)
\mvdash{}  x  \#  c'd'


By

---

Latex:
(RWO  "10<  11<"  (-1)  THEN  Auto)

---

Home Index