---

Step * 1 2 of Lemma r2-plane-separation


1. a : ℝ^2
2. b : ℝ^2
3. u : {u:ℝ^2| r2-left(u;a;b)} 
4. v : {v:ℝ^2| r2-left(v;b;a)} 
5. x : ℝ^2
6. ¬((¬a_b_x) ∧ (¬b_x_a) ∧ (¬x_a_b))
7. u_x_v
⊢ ((¬(d(u;v) < d(u;x))) ∧ (¬(d(u;v) < d(x;v)))) ∧ (¬(r2-left(u;x;v) ∨ r2-left(u;v;x)))
BY
{ (RWO  "r2-be-iff" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  u  :  \{u:\mBbbR{}\^{}2|  r2-left(u;a;b)\} 
4.  v  :  \{v:\mBbbR{}\^{}2|  r2-left(v;b;a)\} 
5.  x  :  \mBbbR{}\^{}2
6.  \mneg{}((\mneg{}a\_b\_x)  \mwedge{}  (\mneg{}b\_x\_a)  \mwedge{}  (\mneg{}x\_a\_b))
7.  u\_x\_v
\mvdash{}  ((\mneg{}(d(u;v)  <  d(u;x)))  \mwedge{}  (\mneg{}(d(u;v)  <  d(x;v))))  \mwedge{}  (\mneg{}(r2-left(u;x;v)  \mvee{}  r2-left(u;v;x)))


By

---

Latex:
(RWO    "r2-be-iff"  (-1)  THEN  Auto)

---

Home Index