---

Step * of Lemma geo-opp-side-iff

∀[e:BasicGeometry]. ∀[A,B,P,Q:Point].
  (P-AB-Q ⇐⇒ ((¬Colinear(A;B;P)) ∧ (¬Colinear(A;B;Q))) ∧ (¬P leftof AB ⇐⇒ ¬Q leftof BA))
BY
{ Auto }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. P-AB-Q
7. ¬P leftof AB
⊢ ¬Q leftof BA

2
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. P-AB-Q
7. ¬Q leftof BA
⊢ ¬P leftof AB

3
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. ¬Colinear(A;B;P)
7. ¬Colinear(A;B;Q)
8. (¬P leftof AB) ⇒ (¬Q leftof BA)
9. (¬P leftof AB) ⇐ ¬Q leftof BA
⊢ P-AB-Q

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[A,B,P,Q:Point].
    (P-AB-Q  \mLeftarrow{}{}\mRightarrow{}  ((\mneg{}Colinear(A;B;P))  \mwedge{}  (\mneg{}Colinear(A;B;Q)))  \mwedge{}  (\mneg{}P  leftof  AB  \mLeftarrow{}{}\mRightarrow{}  \mneg{}Q  leftof  BA))


By

---

Latex:
Auto

---

Home Index