---

Step * 1 1 1 of Lemma lsep-implies-sep-or-lsep


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. a # bc
7. ∀p:Point. (Colinear(a;b;p) ⇒ p ≠ c)
8. u : Point
9. v : Point
10. Colinear(b;a;u)
11. Colinear(b;a;v)
12. u ≠ v
13. xu ≅ xv
14. d : Point
15. u_d_v
16. ud ≅ dv
17. u ≠ d
18. v ≠ d
19. c1 : Point
20. c1v ≅ uv
21. c1u ≅ vu
22. c1u ≅ c1v
23. c1 # vu
24. Colinear(x;c1;d)
25. c1 # du
⊢ c ≠ x ∨ x # ab
BY
{ (Assert Colinear(a;b;d) BY
         EAuto 1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. a # bc
7. ∀p:Point. (Colinear(a;b;p) ⇒ p ≠ c)
8. u : Point
9. v : Point
10. Colinear(b;a;u)
11. Colinear(b;a;v)
12. u ≠ v
13. xu ≅ xv
14. d : Point
15. u_d_v
16. ud ≅ dv
17. u ≠ d
18. v ≠ d
19. c1 : Point
20. c1v ≅ uv
21. c1u ≅ vu
22. c1u ≅ c1v
23. c1 # vu
24. Colinear(x;c1;d)
25. c1 # du
26. Colinear(a;b;d)
⊢ c ≠ x ∨ x # ab

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  a  \#  bc
7.  \mforall{}p:Point.  (Colinear(a;b;p)  {}\mRightarrow{}  p  \mneq{}  c)
8.  u  :  Point
9.  v  :  Point
10.  Colinear(b;a;u)
11.  Colinear(b;a;v)
12.  u  \mneq{}  v
13.  xu  \mcong{}  xv
14.  d  :  Point
15.  u\_d\_v
16.  ud  \mcong{}  dv
17.  u  \mneq{}  d
18.  v  \mneq{}  d
19.  c1  :  Point
20.  c1v  \mcong{}  uv
21.  c1u  \mcong{}  vu
22.  c1u  \mcong{}  c1v
23.  c1  \#  vu
24.  Colinear(x;c1;d)
25.  c1  \#  du
\mvdash{}  c  \mneq{}  x  \mvee{}  x  \#  ab


By

---

Latex:
(Assert  Colinear(a;b;d)  BY
              EAuto  1)

---

Home Index