let r be Real; :: 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 Th7;
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 Th8;
A4: P c= P1 /\ P2

proof

let x be object ; :: 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 A5: ex p being Point of (TOP-REAL 2) st
( p = x & p `2 = r ) by A1;
then A6: x in P1 ;
x in P2 by A5;
hence x in P1 /\ P2 by A6, XBOOLE_0:def 4; :: thesis: verum

end;

P1 /\ P2 c= P

proof

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

end;

then P = P1 /\ P2 by A4;
hence P is closed by A2, A3, TOPS_1:8; :: thesis: verum