let r be real number ; :: thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds
P is closed
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `2 = r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `2 = r } ; :: thesis: P is closed
defpred S<sub>1</sub>[ Point of (TOP-REAL 2)] means $1 `2 >= r;
{ p where p is Element of (TOP-REAL 2) : S₁[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
then reconsider P1 = { p where p is Point of (TOP-REAL 2) : p `2 >= r } as Subset of (TOP-REAL 2) ;
A2: P1 is closed by Th8;
defpred S<sub>2</sub>[ Point of (TOP-REAL 2)] means $1 `2 <= r;
{ p where p is Element of (TOP-REAL 2) : S₂[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch 7();
then reconsider P2 = { p where p is Point of (TOP-REAL 2) : p `2 <= r } as Subset of (TOP-REAL 2) ;
A3: P2 is closed by Th9;
P = P1 /\ P2

proof

A4: P c= P1 /\ P2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in P1 /\ P2 )
assume x in P ; :: thesis: x in P1 /\ P2
then consider p being Point of (TOP-REAL 2) such that
A5: ( p = x & p `2 = r ) by A1;
( x in P1 & x in P2 ) by A5;
hence x in P1 /\ P2 by XBOOLE_0:def 4; :: thesis: verum

end;

P1 /\ P2 c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 /\ P2 or x in P )
assume x in P1 /\ P2 ; :: thesis: x in P
then A6: ( x in P1 & x in P2 ) by XBOOLE_0:def 4;
then consider q1 being Point of (TOP-REAL 2) such that
A7: ( q1 = x & q1 `2 >= r ) ;
consider q2 being Point of (TOP-REAL 2) such that
A8: ( q2 = x & q2 `2 <= r ) by A6;
q1 `2 = r by A7, A8, XXREAL_0:1;
hence x in P by A1, A7; :: thesis: verum

end;

hence P = P1 /\ P2 by A4, XBOOLE_0:def 10; :: thesis: verum

end;

hence P is closed by A2, A3, TOPS_1:35; :: thesis: verum