---

Step * of Lemma eu-colinear-is-colinear-set

∀e:EuclideanPlane. ∀A,B,C:Point.  (Colinear(A;B;C) ⇒ eu-colinear-set(e;[A; B; C]))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (Reduce -1 THEN IntSegCases (-1))
   THEN Reduce 0
   THEN RepeatFor 2 (ProveLAll)
   THEN EAuto 1) }

1
1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. Colinear(A;B;C)
6. i : ℤ
7. i = 0 ∈ ℤ
8. B@0 : Point
9. i1 : ℕ
10. i1 < 3
11. ¬(i1 = 0 ∈ ℤ)
12. ¬(i1 = 1 ∈ ℤ)
13. i1 = 2 ∈ ℤ
14. C@0 : Point
15. i2 : ℕ
16. i2 < 3
17. ¬(i2 = 0 ∈ ℤ)
18. i2 = 1 ∈ ℤ
19. ¬(A = C ∈ Point)
⊢ Colinear(A;C;B)

2
1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. Colinear(A;B;C)
6. i : ℤ
7. i = 1 ∈ ℤ
8. B@0 : Point
9. i1 : ℕ
10. i1 < 3
11. ¬(i1 = 0 ∈ ℤ)
12. ¬(i1 = 1 ∈ ℤ)
13. i1 = 2 ∈ ℤ
14. C@0 : Point
15. i2 : ℕ
16. i2 < 3
17. i2 = 0 ∈ ℤ
18. ¬(B = C ∈ Point)
⊢ Colinear(B;C;A)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C:Point.    (Colinear(A;B;C)  {}\mRightarrow{}  eu-colinear-set(e;[A;  B;  C]))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (Reduce  -1  THEN  IntSegCases  (-1))
  THEN  Reduce  0
  THEN  RepeatFor  2  (ProveLAll)
  THEN  EAuto  1)

---

Home Index