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

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
A2: r > 0 and
A3: Ball u,r c= Int P by TOPMETR:22;
take r = r; :: thesis: ( r > 0 & Ball u,r c= P )
thus r > 0 by A2; :: thesis: Ball u,r c= P
Int P c= P by TOPS_1:44;
hence Ball u,r c= P by A3, XBOOLE_1:1; :: thesis: verum

end;

given r being real number such that A4: r > 0 and
A5: Ball u,r c= P ; :: thesis: u in Int P
A6: u in Ball u,r by A4, Th4;
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 (TopSpaceMetr M) ;
B is open by Lm4;
hence u in Int P by A5, A6, TOPS_1:54; :: thesis: verum