---

Step * 1 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
17. a ≠ b
18. b ≠ c
19. c ≠ a
⊢ False
BY
{ (D -6 THEN BHyp -4  THEN OnMaybeHyp 11 (\h. (ParallelOp h THEN (D 0 THENL [Hypothesis; Auto])))) }

---

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
17.  a  \mneq{}  b
18.  b  \mneq{}  c
19.  c  \mneq{}  a
\mvdash{}  False


By

---

Latex:
(D  -6  THEN  BHyp  -4    THEN  OnMaybeHyp  11  (\mbackslash{}h.  (ParallelOp  h  THEN  (D  0  THENL  [Hypothesis;  Auto]))))

---

Home Index