---

Step * 1 1 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. u_x_v
7. ¬((¬a_b_x) ∧ (¬b_x_a) ∧ (¬x_a_b))
⊢ ¬(r2-left(a;b;x) ∨ r2-left(a;x;b))
BY
{ (RWO "r2-not-left-right-iff" 0 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.  u\_x\_v
7.  \mneg{}((\mneg{}a\_b\_x)  \mwedge{}  (\mneg{}b\_x\_a)  \mwedge{}  (\mneg{}x\_a\_b))
\mvdash{}  \mneg{}(r2-left(a;b;x)  \mvee{}  r2-left(a;x;b))


By

---

Latex:
(RWO  "r2-not-left-right-iff"  0  THEN  Auto)

---

Home Index