let M be non empty MetrSpace; 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; 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); ( u in Int P iff ex r being Real st
( r > 0 & Ball (u,r) c= P ) )
given r being Real such that A3:
r > 0
and
A4:
Ball (u,r) c= P
; 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; verum