let n be Element of NAT ; :: thesis: for w being Point of (Euclid n)
for A being Subset of (TOP-REAL n)
for r being real number st A = Sphere w,r holds
A is closed
let w be Point of (Euclid n); :: thesis: for A being Subset of (TOP-REAL n)
for r being real number st A = Sphere w,r holds
A is closed
let A be Subset of (TOP-REAL n); :: thesis: for r being real number st A = Sphere w,r holds
A is closed
let r be real number ; :: thesis: ( A = Sphere w,r implies A is closed )
A1: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider E = A as Subset of (TopSpaceMetr (Euclid n)) ;
assume A = Sphere w,r ; :: thesis: A is closed
then E is closed by Th68;
hence A is closed by A1, PRE_TOPC:61; :: thesis: verum