---

Step * 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
⊢ c ≠ x ∨ x # ab
BY
{ (((InstLemma `Euclid-midpoint` [⌜e⌝;⌜u⌝;⌜v⌝]⋅ THEN Auto) THEN ExRepD THEN Auto)
   THEN (FLemma `midpoint-sep` [-1] THENA Auto)
   THEN (InstLemma `Euclid-Prop1` [⌜e⌝;⌜u⌝;⌜v⌝]⋅ THEN Auto)
   THEN ExRepD
   THEN D -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. u ≠ d
17. v ≠ d
18. c1 : Point
19. (c1v ≅ uv ∧ c1u ≅ vu) ∧ c1u ≅ c1v
20. c1 # vu
⊢ 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
\mvdash{}  c  \mneq{}  x  \mvee{}  x  \#  ab


By

---

Latex:
(((InstLemma  `Euclid-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD  THEN  Auto)
  THEN  (FLemma  `midpoint-sep`  [-1]  THENA  Auto)
  THEN  (InstLemma  `Euclid-Prop1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  D  -1)

---

Home Index