---

Step * 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. u ≠ d
17. v ≠ d
18. c1 : Point
19. (c1v ≅ uv ∧ c1u ≅ vu) ∧ c1u ≅ c1v
20. c1 # vu
⊢ c ≠ x ∨ x # ab
BY
{ ((D -6 THEN InstLemma `upper-dimension-axiom` [⌜e⌝;⌜x⌝;⌜c1⌝;⌜d⌝;⌜u⌝;⌜v⌝]⋅ THEN Auto) THEN (Assert c1 # du BY Auto)) }

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
⊢ 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.  u  \mneq{}  d
17.  v  \mneq{}  d
18.  c1  :  Point
19.  (c1v  \mcong{}  uv  \mwedge{}  c1u  \mcong{}  vu)  \mwedge{}  c1u  \mcong{}  c1v
20.  c1  \#  vu
\mvdash{}  c  \mneq{}  x  \mvee{}  x  \#  ab


By

---

Latex:
((D  -6  THEN  InstLemma  `upper-dimension-axiom`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Assert  c1  \#  du  BY
                          Auto)
  )

---

Home Index