---

Step * 1 of Lemma geo-colinear-cases


1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. X : ℙ
6. X supposing ¬¬X
7. a ≡ b ⇒ X
8. b ≡ c ⇒ X
9. c ≡ a ⇒ X
10. a-b-c ⇒ X
11. b-c-a ⇒ X
12. c-a-b ⇒ X
13. (¬Colinear(a;b;c)) ⇒ X
14. ¬X
15. Colinear(a;b;c)
16. (a_b_c ⇒ X) ⇒ (b_c_a ⇒ X) ⇒ (c_a_b ⇒ X) ⇒ X
⊢ False
BY
{ ((gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THENA Auto)
   THEN (gSeparatedCases ⌜b⌝ ⌜c⌝⋅ THENA Auto)
   THEN (gSeparatedCases ⌜c⌝ ⌜a⌝⋅ THENA Auto)) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. X : ℙ
6. X supposing ¬¬X
7. a ≡ b ⇒ X
8. b ≡ c ⇒ X
9. c ≡ a ⇒ X
10. a-b-c ⇒ X
11. b-c-a ⇒ X
12. c-a-b ⇒ X
13. (¬Colinear(a;b;c)) ⇒ X
14. ¬X
15. Colinear(a;b;c)
16. (a_b_c ⇒ X) ⇒ (b_c_a ⇒ X) ⇒ (c_a_b ⇒ X) ⇒ X
17. a ≠ b
18. b ≠ c
19. c ≠ a
⊢ False

---

Latex:

---

Latex:

1.  e  :  BasicGeometry-
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  X  :  \mBbbP{}
6.  X  supposing  \mneg{}\mneg{}X
7.  a  \mequiv{}  b  {}\mRightarrow{}  X
8.  b  \mequiv{}  c  {}\mRightarrow{}  X
9.  c  \mequiv{}  a  {}\mRightarrow{}  X
10.  a-b-c  {}\mRightarrow{}  X
11.  b-c-a  {}\mRightarrow{}  X
12.  c-a-b  {}\mRightarrow{}  X
13.  (\mneg{}Colinear(a;b;c))  {}\mRightarrow{}  X
14.  \mneg{}X
15.  Colinear(a;b;c)
16.  (a\_b\_c  {}\mRightarrow{}  X)  {}\mRightarrow{}  (b\_c\_a  {}\mRightarrow{}  X)  {}\mRightarrow{}  (c\_a\_b  {}\mRightarrow{}  X)  {}\mRightarrow{}  X
\mvdash{}  False


By

---

Latex:
((gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gSeparatedCases  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gSeparatedCases  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index