let V be RealUnitarySpace; :: thesis: for M being Subset of (TopUnitSpace V)
for r being Real
for v being Point of V st M = Ball (v,r) holds
M is open
let M be Subset of (TopUnitSpace V); :: thesis: for r being Real
for v being Point of V st M = Ball (v,r) holds
M is open
let r be Real; :: thesis: for v being Point of V st M = Ball (v,r) holds
M is open
let v be Point of V; :: thesis: ( M = Ball (v,r) implies M is open )
assume M = Ball (v,r) ; :: thesis: M is open
then M in Family_open_set V by Th37;
hence M is open by PRE_TOPC:def 2; :: thesis: verum