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
A2: 2 in Seg 2 by FINSEQ_1:1;
A3: P ` c= { p where p is Point of () : p `2 < r }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P ` or x in { p where p is Point of () : p `2 < r } )
assume A4: x in P ` ; :: thesis: x in { p where p is Point of () : p `2 < r }
then x in the carrier of () \ P by SUBSET_1:def 4;
then A5: not x in P by XBOOLE_0:def 5;
reconsider q = x as Point of () by A4;
q `2 < r by A1, A5;
hence x in { p where p is Point of () : p `2 < r } ; :: thesis: verum
end;
{ p where p is Point of () : p `2 < r } c= P `
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : p `2 < r } or x in P ` )
assume x in { p where p is Point of () : p `2 < r } ; :: thesis: x in P `
then A6: ex p being Point of () st
( p = x & p `2 < r ) ;
now :: thesis: not x in { q where q is Point of () : q `2 >= r }
assume x in { q where q is Point of () : q `2 >= r } ; :: thesis: contradiction
then ex q being Point of () st
( q = x & q `2 >= r ) ;
hence contradiction by A6; :: thesis: verum
end;
then x in the carrier of () \ P by ;
hence x in P ` by SUBSET_1:def 4; :: thesis: verum
end;
then A7: P ` = { p where p is Point of () : p `2 < r } by A3;
A8: P ` c= { p where p is Point of () : r > p /. 2 }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P ` or x in { p where p is Point of () : r > p /. 2 } )
assume x in P ` ; :: thesis: x in { p where p is Point of () : r > p /. 2 }
then consider p being Point of () such that
A9: p = x and
A10: p `2 < r by A7;
p /. 2 < r by ;
hence x in { p where p is Point of () : r > p /. 2 } by A9; :: thesis: verum
end;
{ p where p is Point of () : r > p /. 2 } c= P `
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : r > p /. 2 } or x in P ` )
assume x in { p where p is Point of () : r > p /. 2 } ; :: thesis: x in P `
then consider q being Point of () such that
A11: q = x and
A12: r > q /. 2 ;
q `2 < r by ;
hence x in P ` by ; :: thesis: verum
end;
then A13: P ` = { p where p is Point of () : r > p /. 2 } by A8;
reconsider P1 = P ` as Subset of () ;
P1 is open by ;
hence P is closed by TOPS_1:3; :: thesis: verum