let n be Element of 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 number 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 number 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 number st
( r > 0 & Ball u,r c= P ) )
XX: 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 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 XX, LmX; :: thesis: verum