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 P9 = P as Subset of M ;
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 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 )
then P in the topology of (TopSpaceMetr M) by PRE_TOPC:def 2;
then A1: P9 in Family_open_set M ;
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 p in P ; :: thesis: ex r being real number st
( r > 0 & Ball (p,r) c= P )
then ex r being Real st
( r > 0 & Ball (p,r) c= P ) by A1, PCOMPS_1:def 4;
hence ex r being real number st
( r > 0 & Ball (p,r) c= P ) ; :: thesis: verum

end;

assume A2: 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
A3: ( r > 0 & Ball (p,r) c= P ) by A2;
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 A3; :: thesis: verum

end;

then P9 in Family_open_set M by PCOMPS_1:def 4;
hence P in the topology of (TopSpaceMetr M) ; :: according to PRE_TOPC:def 2 :: thesis: verum