let r be Real; :: thesis: for P being Subset of () st P = { p where p is Point of () : p `2 = r } holds
P is closed

let P be Subset of (); :: thesis: ( P = { p where p is Point of () : p `2 = r } implies P is closed )
assume A1: P = { p where p is Point of () : p `2 = r } ; :: thesis: P is closed
defpred S1[ Point of ()] means \$1 `2 >= r;
{ p where p is Element of () : S1[p] } is Subset of () from then reconsider P1 = { p where p is Point of () : p `2 >= r } as Subset of () ;
A2: P1 is closed by Th7;
defpred S2[ Point of ()] means \$1 `2 <= r;
{ p where p is Element of () : S2[p] } is Subset of () from then reconsider P2 = { p where p is Point of () : p `2 <= r } as Subset of () ;
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 () st
( p = x & p `2 = r ) by A1;
then A6: x in P1 ;
x in P2 by A5;
hence x in P1 /\ P2 by ; :: 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 ;
consider q1 being Point of () such that
A10: q1 = x and
A11: q1 `2 >= r by A8;
ex q2 being Point of () st
( q2 = x & q2 `2 <= r ) by A9;
then q1 `2 = r by ;
hence x in P by ; :: thesis: verum
end;
then P = P1 /\ P2 by A4;
hence P is closed by ; :: thesis: verum