---

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


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)
BY
{ (StableCases ⌜C = A ∈ Point⌝⋅ THENA Auto) }

1
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)
19. C = A ∈ Point
⊢ Colinear(B;C;A)

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)
19. ¬(C = A ∈ Point)
⊢ Colinear(B;C;A)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  Colinear(A;B;C)
6.  i  :  \mBbbZ{}
7.  i  =  1
8.  B@0  :  Point
9.  i1  :  \mBbbN{}
10.  i1  <  3
11.  \mneg{}(i1  =  0)
12.  \mneg{}(i1  =  1)
13.  i1  =  2
14.  C@0  :  Point
15.  i2  :  \mBbbN{}
16.  i2  <  3
17.  i2  =  0
18.  \mneg{}(B  =  C)
\mvdash{}  Colinear(B;C;A)


By

---

Latex:
(StableCases  \mkleeneopen{}C  =  A\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index