---

Step * of Lemma r2-nontrivial

No Annotations
∃a:ℝ^2. (∃b:ℝ^2 [(d(a;a) < d(a;b))])
BY
{ ((InstLemma `rv-sep-exists` [⌜2⌝]⋅ THEN Auto) THEN ParallelLast THEN D -1) }

1
1. a : ℝ^2
2. b : ℝ^2
3. a ≠ b
⊢ ∃b:ℝ^2 [(d(a;a) < d(a;b))]

---

Latex:

---

Latex:
No  Annotations
\mexists{}a:\mBbbR{}\^{}2.  (\mexists{}b:\mBbbR{}\^{}2  [(d(a;a)  <  d(a;b))])


By

---

Latex:
((InstLemma  `rv-sep-exists`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ParallelLast  THEN  D  -1)

---

Home Index