---

Step * of Lemma 2opp-side-implies-same-side

∀e:BasicGeometry. ∀a,c,d,p,q:Point.
  (((geo-tar-opp-side(e;a;d;p;q) ∧ geo-tar-opp-side(e;c;d;p;q)) ∧ a ≠ c) ⇒ geo-tar-same-side(e;a;c;p;q))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. c : Point
4. d : Point
5. p : Point
6. q : Point
7. geo-tar-opp-side(e;a;d;p;q)
8. geo-tar-opp-side(e;c;d;p;q)
9. a ≠ c
⊢ geo-tar-same-side(e;a;c;p;q)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,c,d,p,q:Point.
    (((geo-tar-opp-side(e;a;d;p;q)  \mwedge{}  geo-tar-opp-side(e;c;d;p;q))  \mwedge{}  a  \mneq{}  c)
    {}\mRightarrow{}  geo-tar-same-side(e;a;c;p;q))


By

---

Latex:
Auto

---

Home Index