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 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 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 st
( r > 0 & Ball (u,r) c= P ) )
hereby :: thesis: ( ex r being Real st
( r > 0 & Ball (u,r) c= P ) implies u in Int P )
assume u in Int P ; :: thesis: ex r being Real st
( r > 0 & Ball (u,r) c= P )
then consider r being Real such that
A1: r > 0 and
A2: Ball (u,r) c= Int P by TOPMETR:15;
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:16;
hence Ball (u,r) c= P by A2; :: thesis: verum
end;
given r being Real 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 5;
then reconsider B = Ball (u,r) as Subset of (TopSpaceMetr M) ;
A5: B is open by Lm4;
u in Ball (u,r) by A3, Th1;
hence u in Int P by A4, A5, TOPS_1:22; :: thesis: verum