let M be non empty MetrSpace; :: thesis: for P being Subset of (TopSpaceMetr M) holds
( P is open iff for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball p,r c= P ) )
let P be Subset of (TopSpaceMetr M); :: thesis: ( P is open iff for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball p,r c= P ) )
reconsider P' = P as Subset of M by Th16;
thus ( P is open implies for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball p,r c= P ) ) :: thesis: ( ( for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball p,r c= P ) ) implies P is open )

proof

assume A1: P is open ; :: thesis: for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball p,r c= P )
let p be Point of M; :: thesis: ( p in P implies ex r being real number st
( r > 0 & Ball p,r c= P ) )
assume A2: p in P ; :: thesis: ex r being real number st
( r > 0 & Ball p,r c= P )
P in the topology of (TopSpaceMetr M) by A1, PRE_TOPC:def 5;
then P' in Family_open_set M by Th16;
then ex r being Real st
( r > 0 & Ball p,r c= P ) by A2, PCOMPS_1:def 5;
hence ex r being real number st
( r > 0 & Ball p,r c= P ) ; :: thesis: verum

end;

assume A3: for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball p,r c= P ) ; :: thesis: P is open
for p being Point of M st p in P holds
ex r being Real st
( r > 0 & Ball p,r c= P )

proof

let p be Point of M; :: thesis: ( p in P implies ex r being Real st
( r > 0 & Ball p,r c= P ) )
assume p in P ; :: thesis: ex r being Real st
( r > 0 & Ball p,r c= P )
then consider r being real number such that
A4: ( r > 0 & Ball p,r c= P ) by A3;
reconsider r = r as Element of REAL by XREAL_0:def 1;
take r ; :: thesis: ( r > 0 & Ball p,r c= P )
thus ( r > 0 & Ball p,r c= P ) by A4; :: thesis: verum

end;

then P' in Family_open_set M by PCOMPS_1:def 5;
hence P in the topology of (TopSpaceMetr M) by Th16; :: according to PRE_TOPC:def 5 :: thesis: verum