let V be RealUnitarySpace; :: thesis: for M being Subset of
for r being Real
for v being Point of st M = Ball v,r holds
M is open
let M be Subset of ; :: thesis: for r being Real
for v being Point of st M = Ball v,r holds
M is open
let r be Real; :: thesis: for v being Point of st M = Ball v,r holds
M is open
let v be Point of ; :: 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