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 5; :: thesis: verum