---

Step * 1 1 of Lemma geo-line-eq_transitivity


1. g : EuclideanPlane
2. l : Line
3. m : Line
4. n : Line
5. l ≡ m
6. m ≡ n
7. p : Point
8. Colinear(p;fst(l);fst(snd(l)))
9. p # fst(n)fst(snd(n))
10. Colinear(fst(l);fst(snd(l));fst(m))
11. Colinear(fst(l);fst(snd(l));fst(snd(m)))
12. Colinear(fst(m);fst(snd(m));fst(n))
13. Colinear(fst(m);fst(snd(m));fst(snd(n)))
⊢ False
BY
{ (((D 2 THEN D 3) THEN (D 5 THEN D 6) THEN D 8 THEN D 9) THEN All Reduce⋅) }

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)
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  l  :  Line
3.  m  :  Line
4.  n  :  Line
5.  l  \mequiv{}  m
6.  m  \mequiv{}  n
7.  p  :  Point
8.  Colinear(p;fst(l);fst(snd(l)))
9.  p  \#  fst(n)fst(snd(n))
10.  Colinear(fst(l);fst(snd(l));fst(m))
11.  Colinear(fst(l);fst(snd(l));fst(snd(m)))
12.  Colinear(fst(m);fst(snd(m));fst(n))
13.  Colinear(fst(m);fst(snd(m));fst(snd(n)))
\mvdash{}  False


By

---

Latex:
(((D  2  THEN  D  3)  THEN  (D  5  THEN  D  6)  THEN  D  8  THEN  D  9)  THEN  All  Reduce\mcdot{})

---

Home Index