---

Step * of Lemma r2-plane-separation1

No Annotations
∀a,b:ℝ^2. ∀u:{u:ℝ^2| r2-left(u;a;b)} . ∀v:{v:ℝ^2| r2-left(v;b;a)} .
  (∃x:ℝ^2 [((¬((¬a_b_x) ∧ (¬b_x_a) ∧ (¬x_a_b))) ∧ u_x_v)])
BY
{ (Auto THEN (InstLemma `r2-left-right` [⌜a⌝;⌜b⌝;⌜u⌝;⌜v⌝]⋅ THENA Auto) THEN D -1 THEN D 0 With ⌜z⌝  THEN Auto) }

1
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. z : ℝ^2
6. rv-T(2;u;z;v)
7. ¬rv-pos-angle(2;z;a;b)
⊢ ¬((¬a_b_z) ∧ (¬b_z_a) ∧ (¬z_a_b))

2
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. z : ℝ^2
6. rv-T(2;u;z;v)
7. ¬rv-pos-angle(2;z;a;b)
8. ¬((¬a_b_z) ∧ (¬b_z_a) ∧ (¬z_a_b))
⊢ u_z_v

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:\mBbbR{}\^{}2.  \mforall{}u:\{u:\mBbbR{}\^{}2|  r2-left(u;a;b)\}  .  \mforall{}v:\{v:\mBbbR{}\^{}2|  r2-left(v;b;a)\}  .
    (\mexists{}x:\mBbbR{}\^{}2  [((\mneg{}((\mneg{}a\_b\_x)  \mwedge{}  (\mneg{}b\_x\_a)  \mwedge{}  (\mneg{}x\_a\_b)))  \mwedge{}  u\_x\_v)])


By

---

Latex:
(Auto
  THEN  (InstLemma  `r2-left-right`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}z\mkleeneclose{} 
  THEN  Auto)

---

Home Index