let n be Nat; :: thesis: for r being Real
for B being Subset of (TOP-REAL n)
for u being Point of (Euclid n) st B = Ball (u,r) holds
B is open
let r be Real; :: thesis: for B being Subset of (TOP-REAL n)
for u being Point of (Euclid n) st B = Ball (u,r) holds
B is open
let B be Subset of (TOP-REAL n); :: thesis: for u being Point of (Euclid n) st B = Ball (u,r) holds
B is open
let u be Point of (Euclid n); :: thesis: ( B = Ball (u,r) implies B is open )
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider BB = B as Subset of (TopSpaceMetr (Euclid n)) ;
assume B = Ball (u,r) ; :: thesis: B is open
then BB is open by Lm4;
hence B is open by A1, PRE_TOPC:30; :: thesis: verum