---

Step * 1 of Lemma weak-same-side-invariant

.....assertion..... 
1. [e] : BasicGeometry
⊢ ∀[A,B,C:Point].
    (¬¬(((∀P:Point. (P leftof AB ⇐⇒ P leftof CB)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof BC)))
       ∨ ((∀P:Point. (P leftof AB ⇐⇒ P leftof BC)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof CB))))) supposing 
       (A ≠ B and 
       C ≠ B and 
       Colinear(B;C;A))
BY
{ ((Intros THEN (D 0 THENA Auto)) THEN Unhide THEN gSimpleColinearCases (-4)) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. Colinear(B;C;A)
6. C ≠ B
7. A ≠ B
8. ¬(((∀P:Point. (P leftof AB ⇐⇒ P leftof CB)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof BC)))
∨ ((∀P:Point. (P leftof AB ⇐⇒ P leftof BC)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof CB))))
9. B_C_A
⊢ False

2
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. Colinear(B;C;A)
6. C ≠ B
7. A ≠ B
8. ¬(((∀P:Point. (P leftof AB ⇐⇒ P leftof CB)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof BC)))
∨ ((∀P:Point. (P leftof AB ⇐⇒ P leftof BC)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof CB))))
9. C_A_B
⊢ False

3
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. Colinear(B;C;A)
6. C ≠ B
7. A ≠ B
8. ¬(((∀P:Point. (P leftof AB ⇐⇒ P leftof CB)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof BC)))
∨ ((∀P:Point. (P leftof AB ⇐⇒ P leftof BC)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof CB))))
9. A_B_C
⊢ False

---

Latex:

---

Latex:
.....assertion..... 
1.  [e]  :  BasicGeometry
\mvdash{}  \mforall{}[A,B,C:Point].
        (\mneg{}\mneg{}(((\mforall{}P:Point.  (P  leftof  AB  \mLeftarrow{}{}\mRightarrow{}  P  leftof  CB))  \mwedge{}  (\mforall{}P:Point.  (P  leftof  BA  \mLeftarrow{}{}\mRightarrow{}  P  leftof  BC)))
              \mvee{}  ((\mforall{}P:Point.  (P  leftof  AB  \mLeftarrow{}{}\mRightarrow{}  P  leftof  BC))
                  \mwedge{}  (\mforall{}P:Point.  (P  leftof  BA  \mLeftarrow{}{}\mRightarrow{}  P  leftof  CB)))))  supposing 
              (A  \mneq{}  B  and 
              C  \mneq{}  B  and 
              Colinear(B;C;A))


By

---

Latex:
((Intros  THEN  (D  0  THENA  Auto))  THEN  Unhide  THEN  gSimpleColinearCases  (-4))

---

Home Index