let n be Nat; :: thesis: for w being Point of (Euclid n)
for A being Subset of (TOP-REAL n)
for r being Real 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 st A = Sphere (w,r) holds
A is closed
let A be Subset of (TOP-REAL n); :: thesis: for r being Real st A = Sphere (w,r) holds
A is closed
let r be Real; :: 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 Th58;
hence A is closed by A1, PRE_TOPC:31; :: thesis: verum