---

Step * of Lemma ip-non-trivial

∀rv:InnerProductSpace. ∀x:{x:Point| r0 < ||x||} .  ∃a:Point. (∃b:{Point| a # b})
BY
{ (Auto THEN (D 0 With ⌜x⌝  THENA Auto)) }

1
1. rv : InnerProductSpace
2. x : {x:Point| r0 < ||x||} 
⊢ ∃b:{Point| x # b}

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}x:\{x:Point|  r0  <  ||x||\}  .    \mexists{}a:Point.  (\mexists{}b:\{Point|  a  \#  b\})


By

---

Latex:
(Auto  THEN  (D  0  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto))

---

Home Index