---

Step * of Lemma r2-sep-or

No Annotations
∀a:ℝ^2. ∀b:{b:ℝ^2| d(a;a) < d(a;b)} . ∀c:ℝ^2.  ((d(a;a) < d(a;c)) ∨ (d(b;b) < d(b;c)))
BY
{ (Auto
   THEN (RWO "real-vec-dist-same-zero" 0 THENA Auto)
   THEN Fold `real-vec-sep` 0
   THEN BLemma `real-vec-sep-cases-alt`
   THEN Auto) }

1
1. a : ℝ^2
2. b : {b:ℝ^2| d(a;a) < d(a;b)} 
3. c : ℝ^2
⊢ a ≠ b

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:\mBbbR{}\^{}2.  \mforall{}b:\{b:\mBbbR{}\^{}2|  d(a;a)  <  d(a;b)\}  .  \mforall{}c:\mBbbR{}\^{}2.    ((d(a;a)  <  d(a;c))  \mvee{}  (d(b;b)  <  d(b;c)))


By

---

Latex:
(Auto
  THEN  (RWO  "real-vec-dist-same-zero"  0  THENA  Auto)
  THEN  Fold  `real-vec-sep`  0
  THEN  BLemma  `real-vec-sep-cases-alt`
  THEN  Auto)

---

Home Index