---

Step * of Lemma geo-tar-opp-side-iff

∀e:BasicGeometry. ∀A,B,P,Q:Point.  (geo-tar-opp-side(e;P;Q;A;B) ⇐⇒ P # AB ∧ Q # AB ∧ (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. geo-tar-opp-side(e;P;Q;A;B)
7. P leftof AB
⊢ Q leftof BA

2
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. geo-tar-opp-side(e;P;Q;A;B)
7. Q leftof BA
⊢ P leftof AB

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

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,P,Q:Point.
    (geo-tar-opp-side(e;P;Q;A;B)  \mLeftarrow{}{}\mRightarrow{}  P  \#  AB  \mwedge{}  Q  \#  AB  \mwedge{}  (P  leftof  AB  \mLeftarrow{}{}\mRightarrow{}  Q  leftof  BA))


By

---

Latex:
Auto

---

Home Index