let n be Element of 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 )
XX: 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 XX, PRE_TOPC:60; :: thesis: verum