---

Step * 1 1 1 of Lemma geo-line-eq_transitivity


1. g : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. x1 : Point
6. y1 : Point
7. m2 : x1 ≠ y1
8. x2 : Point
9. y2 : Point
10. n2 : x2 ≠ y2
11. <x, y, l2> ≡ <x1, y1, m2>
12. <x1, y1, m2> ≡ <x2, y2, n2>
13. p : Point
14. Colinear(p;x;y)
15. p # x2y2
16. Colinear(x;y;x1)
17. Colinear(x;y;y1)
18. Colinear(x1;y1;x2)
19. Colinear(x1;y1;y2)
⊢ False
BY
{ ((Assert Colinear(x2;x;y) BY ProveGeoColinear) THEN (Assert Colinear(y2;x;y) BY ProveGeoColinear)) }

1
1. g : EuclideanPlane
2. x : Point
3. y : Point
4. l2 : x ≠ y
5. x1 : Point
6. y1 : Point
7. m2 : x1 ≠ y1
8. x2 : Point
9. y2 : Point
10. n2 : x2 ≠ y2
11. <x, y, l2> ≡ <x1, y1, m2>
12. <x1, y1, m2> ≡ <x2, y2, n2>
13. p : Point
14. Colinear(p;x;y)
15. p # x2y2
16. Colinear(x;y;x1)
17. Colinear(x;y;y1)
18. Colinear(x1;y1;x2)
19. Colinear(x1;y1;y2)
20. Colinear(x2;x;y)
21. Colinear(y2;x;y)
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  x  :  Point
3.  y  :  Point
4.  l2  :  x  \mneq{}  y
5.  x1  :  Point
6.  y1  :  Point
7.  m2  :  x1  \mneq{}  y1
8.  x2  :  Point
9.  y2  :  Point
10.  n2  :  x2  \mneq{}  y2
11.  <x,  y,  l2>  \mequiv{}  <x1,  y1,  m2>
12.  <x1,  y1,  m2>  \mequiv{}  <x2,  y2,  n2>
13.  p  :  Point
14.  Colinear(p;x;y)
15.  p  \#  x2y2
16.  Colinear(x;y;x1)
17.  Colinear(x;y;y1)
18.  Colinear(x1;y1;x2)
19.  Colinear(x1;y1;y2)
\mvdash{}  False


By

---

Latex:
((Assert  Colinear(x2;x;y)  BY  ProveGeoColinear)  THEN  (Assert  Colinear(y2;x;y)  BY  ProveGeoColinear))

---

Home Index