---

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

∀e:BasicGeometry. ∀A,B,P,Q:Point.  (geo-tar-same-side(e;P;Q;A;B) ⇐⇒ P # AB ∧ Q # AB ∧ (P leftof AB ⇐⇒ Q leftof AB))
BY
{ ((UnivCD THENA Auto) THEN (RepeatFor 2 (D 0) THENA Auto)) }

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

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index