let M be non empty MetrSpace; :: thesis: for u being Point of
for P being Subset of holds
( u in Int P iff ex r being real number st
( r > 0 & Ball u,r c= P ) )
let u be Point of ; :: thesis: for P being Subset of holds
( u in Int P iff ex r being real number st
( r > 0 & Ball u,r c= P ) )
let P be Subset of ; :: thesis: ( u in Int P iff ex r being real number st
( r > 0 & Ball u,r c= P ) )

hereby :: thesis: ( ex r being real number st
( r > 0 & Ball u,r c= P ) implies u in Int P )

assume u in Int P ; :: thesis: ex r being real number st
( r > 0 & Ball u,r c= P )
then consider r being real number such that
A1: r > 0 and
A2: Ball u,r c= Int P by TOPMETR:22;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P )
thus r > 0 by A1; :: thesis: Ball u,r c= P
Int P c= P by TOPS_1:44;
hence Ball u,r c= P by A2, XBOOLE_1:1; :: thesis: verum

end;

given r being real number such that A3: r > 0 and
A4: Ball u,r c= P ; :: thesis: u in Int P
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 6;
then reconsider B = Ball u,r as Subset of ;
A5: B is open by Lm4;
u in Ball u,r by A3, Th4;
hence u in Int P by A4, A5, TOPS_1:54; :: thesis: verum