---

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


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. a ≠ x
9. b ≠ x
⊢ c ≠ x ∨ (¬Colinear(a;b;x))
BY
{ (((gProperProlong ⌜b⌝⌜a⌝`a1'⌜a⌝⌜x⌝⋅ THEN Auto) THEN gProperProlong ⌜a1⌝⌜a⌝`a2'⌜a⌝⌜x⌝⋅ THEN Auto)
   THEN (gProperProlong ⌜a⌝⌜b⌝`b1'⌜b⌝⌜x⌝⋅ THEN Auto)
   THEN gProperProlong ⌜b1⌝⌜b⌝`b2'⌜b⌝⌜x⌝⋅
   THEN 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. a ≠ x
9. b ≠ x
10. a1 : Point
11. b-a-a1
12. aa1 ≅ ax
13. a2 : Point
14. a1-a-a2
15. aa2 ≅ ax
16. b1 : Point
17. a-b-b1
18. bb1 ≅ bx
19. b2 : Point
20. b1-b-b2
21. bb2 ≅ bx
⊢ c ≠ x ∨ (¬Colinear(a;b;x))

---

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.  a  \mneq{}  x
9.  b  \mneq{}  x
\mvdash{}  c  \mneq{}  x  \mvee{}  (\mneg{}Colinear(a;b;x))


By

---

Latex:
(((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`a1'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  gProperProlong  \mkleeneopen{}a1\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`a2'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`b1'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  gProperProlong  \mkleeneopen{}b1\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}`b2'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index