---

Step * of Lemma weak-same-side-invariant

∀[e:BasicGeometry]. ∀[A,B,C,D:Point].
  (¬¬(((∀P:Point. (P leftof AB ⇐⇒ P leftof CD)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof DC)))
     ∨ ((∀P:Point. (P leftof AB ⇐⇒ P leftof DC)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof CD))))) supposing 
     (A ≠ B and 
     C ≠ D and 
     Colinear(C;A;B) and 
     Colinear(D;A;B))
BY
{ (Intro
   THEN Assert ⌜∀[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))⌝⋅
   ) }

1
.....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))

2
1. [e] : BasicGeometry
2. ∀[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))
⊢ ∀[A,B,C,D:Point].
    (¬¬(((∀P:Point. (P leftof AB ⇐⇒ P leftof CD)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof DC)))
       ∨ ((∀P:Point. (P leftof AB ⇐⇒ P leftof DC)) ∧ (∀P:Point. (P leftof BA ⇐⇒ P leftof CD))))) supposing 
       (A ≠ B and 
       C ≠ D and 
       Colinear(C;A;B) and 
       Colinear(D;A;B))

---

Latex:

---

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


By

---

Latex:
(Intro
  THEN  Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}
  )

---

Home Index