let n be Nat; :: thesis: for u being Point of (Euclid n)
for P being Subset of (TOP-REAL n) holds
( u in Int P iff ex r being Real st
( r > 0 & Ball (u,r) c= P ) )
let u be Point of (Euclid n); :: thesis: for P being Subset of (TOP-REAL n) holds
( u in Int P iff ex r being Real st
( r > 0 & Ball (u,r) c= P ) )
let P be Subset of (TOP-REAL n); :: thesis: ( u in Int P iff ex r being Real 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 (TopSpaceMetr (Euclid n)) ;
( u in Int PP iff ex r being Real st
( r > 0 & Ball (u,r) c= PP ) ) by Th4;
hence ( u in Int P iff ex r being Real st
( r > 0 & Ball (u,r) c= P ) ) by A1, Lm5; :: thesis: verum