let V be RealUnitarySpace; :: thesis: for M being Subset of (TopUnitSpace V) holds
( M is open iff for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball v,r c= M ) )
let M be Subset of (TopUnitSpace V); :: thesis: ( M is open iff for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball v,r c= M ) )
thus ( M is open implies for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball v,r c= M ) ) :: thesis: ( ( for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball v,r c= M ) ) implies M is open )

proof

assume M is open ; :: thesis: for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball v,r c= M )
then A1: M in the topology of (TopUnitSpace V) by PRE_TOPC:def 5;
let v be Point of V; :: thesis: ( v in M implies ex r being Real st
( r > 0 & Ball v,r c= M ) )
assume v in M ; :: thesis: ex r being Real st
( r > 0 & Ball v,r c= M )
hence ex r being Real st
( r > 0 & Ball v,r c= M ) by A1, Def5; :: thesis: verum

end;

assume for v being Point of V st v in M holds
ex r being Real st
( r > 0 & Ball v,r c= M ) ; :: thesis: M is open
hence M in the topology of (TopUnitSpace V) by Def5; :: according to PRE_TOPC:def 5 :: thesis: verum