let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)
for a being Real 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 st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
( A ` is open & A is closed )
let a be Real; :: 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 ;
A2: 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)) ;
for p being Point of (Euclid n) st p in P1 holds
ex r being Real st
( r > 0 & Ball (p,r) c= P1 )

proof

let p be Point of (Euclid n); :: thesis: ( p in P1 implies ex r being Real st
( r > 0 & Ball (p,r) c= P1 ) )
reconsider q1 = p as Point of (TOP-REAL n) by TOPREAL3:8;
assume p in P1 ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= P1 )
then not p in A by XBOOLE_0:def 5;
then A3: |.q1.| <> a by A1;

now :: thesis: ( ( |.q1.| <= a & ex r being Real st
( r > 0 & Ball (p,r) c= P1 ) ) or ( |.q1.| > a & ex r being Real st
( r > 0 & Ball (p,r) c= P1 ) ) )

per cases ( |.q1.| <= a or |.q1.| > a ) ;

case A4: |.q1.| <= a ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= P1 )

set r1 = (a - |.q1.|) / 2;
|.q1.| < a by A3, A4, XXREAL_0:1;
then A5: a - |.q1.| > 0 by XREAL_1:50;
Ball (p,((a - |.q1.|) / 2)) c= P1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,((a - |.q1.|) / 2)) or x in P1 )
assume A6: x in Ball (p,((a - |.q1.|) / 2)) ; :: thesis: x in P1
then reconsider p2 = x as Point of (Euclid n) ;
reconsider q2 = p2 as Point of (TOP-REAL n) by TOPREAL3:8;
dist (p,p2) < (a - |.q1.|) / 2 by A6, METRIC_1:11;
then A7: |.(q2 - q1).| < (a - |.q1.|) / 2 by JGRAPH_1:28;

now :: thesis: not q2 in A

assume q2 in A ; :: thesis: contradiction
then A8: ex q being Point of (TOP-REAL n) st
( q = q2 & |.q.| = a ) by A1;
|.(q2 - q1).| >= |.q2.| - |.q1.| by TOPRNS_1:32;
then (a - |.q1.|) / 2 > ((a - |.q1.|) / 2) + ((a - |.q1.|) / 2) by A7, A8, XXREAL_0:2;
then ((a - |.q1.|) / 2) - ((a - |.q1.|) / 2) > (a - |.q1.|) / 2 by XREAL_1:20;
hence contradiction by A5; :: thesis: verum

end;

hence x in P1 by XBOOLE_0:def 5; :: thesis: verum

end;

hence ex r being Real st
( r > 0 & Ball (p,r) c= P1 ) by A5, XREAL_1:139; :: thesis: verum

end;

case A9: |.q1.| > a ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= P1 )

set r1 = (|.q1.| - a) / 2;
A10: |.q1.| - a > 0 by A9, XREAL_1:50;
Ball (p,((|.q1.| - a) / 2)) c= P1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,((|.q1.| - a) / 2)) or x in P1 )
assume A11: x in Ball (p,((|.q1.| - a) / 2)) ; :: thesis: x in P1
then reconsider p2 = x as Point of (Euclid n) ;
reconsider q2 = p2 as Point of (TOP-REAL n) by TOPREAL3:8;
dist (p,p2) < (|.q1.| - a) / 2 by A11, METRIC_1:11;
then A12: |.(q1 - q2).| < (|.q1.| - a) / 2 by JGRAPH_1:28;

now :: thesis: not q2 in A

assume q2 in A ; :: thesis: contradiction
then A13: ex q being Point of (TOP-REAL n) st
( q = q2 & |.q.| = a ) by A1;
|.(q1 - q2).| >= |.q1.| - |.q2.| by TOPRNS_1:32;
then (|.q1.| - a) / 2 > ((|.q1.| - a) / 2) + ((|.q1.| - a) / 2) by A12, A13, XXREAL_0:2;
then ((|.q1.| - a) / 2) - ((|.q1.| - a) / 2) > (|.q1.| - a) / 2 by XREAL_1:20;
hence contradiction by A10; :: thesis: verum

end;

hence x in P1 by XBOOLE_0:def 5; :: thesis: verum

end;

hence ex r being Real st
( r > 0 & Ball (p,r) c= P1 ) by A10, XREAL_1:139; :: thesis: verum

end;

end;

end;

hence ex r being Real st
( r > 0 & Ball (p,r) c= P1 ) ; :: thesis: verum

end;

then P1 is open by TOPMETR:15;
hence A ` is open by A2, PRE_TOPC:30; :: thesis: A is closed
hence A is closed by TOPS_1:3; :: thesis: verum