let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n)
for a being real number st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
( A ` is open & A is closed )
let A be Subset of (TOP-REAL n); :: thesis: for a being real number st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
( A ` is open & A is closed )
let a be real number ; :: thesis: ( A = { q where q is Point of (TOP-REAL n) : |.q.| = a } implies ( A ` is open & A is closed ) )
assume A1:
A = { q where q is Point of (TOP-REAL n) : |.q.| = a }
; :: thesis: ( A ` is open & A is closed )
reconsider a = a as Real by XREAL_0:def 1;
V:
TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider P1 = A ` as Subset of (TopSpaceMetr (Euclid n)) by XX, YY;
for p being Point of (Euclid n) st p in P1 holds
ex r being real number st
( r > 0 & Ball p,r c= P1 )
then
P1 is open
by TOPMETR:22;
hence
A ` is open
by V, PRE_TOPC:60; :: thesis: A is closed
hence
A is closed
by TOPS_1:29; :: thesis: verum