---

Step * of Lemma geo-same-side-iff

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

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

2
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. P,Q-AB
7. ¬Q leftof AB
⊢ ¬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 AB)
9. (¬P leftof AB) ⇐ ¬Q leftof AB
⊢ P,Q-AB

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index