let n be Element of NAT ; :: 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 ) )
A1: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider PP = P as Subset of ;
( u in Int PP iff ex r being real number st
( r > 0 & Ball u,r c= PP ) ) by Th7;
hence ( u in Int P iff ex r being real number st
( r > 0 & Ball u,r c= P ) ) by A1, Lm5; :: thesis: verum