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
A2: 2 in Seg 2 by FINSEQ_1:1;
A3: P ` c= { p where p is Point of (TOP-REAL 2) : 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 (TOP-REAL 2) : p `2 < r } )
assume A4: x in P ` ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : p `2 < r }
then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def 4;
then A5: not x in P by XBOOLE_0:def 5;
reconsider q = x as Point of (TOP-REAL 2) by A4;
q `2 < r by A1, A5;
hence x in { p where p is Point of (TOP-REAL 2) : p `2 < r } ; :: thesis: verum

end;

{ p where p is Point of (TOP-REAL 2) : 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 (TOP-REAL 2) : p `2 < r } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : p `2 < r } ; :: thesis: x in P `
then A6: ex p being Point of (TOP-REAL 2) st
( p = x & p `2 < r ) ;

now :: thesis: not x in { q where q is Point of (TOP-REAL 2) : q `2 >= r }

assume x in { q where q is Point of (TOP-REAL 2) : q `2 >= r } ; :: thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( q = x & q `2 >= r ) ;
hence contradiction by A6; :: thesis: verum

end;

then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def 5;
hence x in P ` by SUBSET_1:def 4; :: thesis: verum

end;

then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `2 < r } by A3;
A8: P ` c= { p where p is Point of (TOP-REAL 2) : 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 (TOP-REAL 2) : r > p /. 2 } )
assume x in P ` ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 }
then consider p being Point of (TOP-REAL 2) such that
A9: p = x and
A10: p `2 < r by A7;
p /. 2 < r by A10, JORDAN2B:29;
hence x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } by A9; :: thesis: verum

end;

{ p where p is Point of (TOP-REAL 2) : 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 (TOP-REAL 2) : r > p /. 2 } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } ; :: thesis: x in P `
then consider q being Point of (TOP-REAL 2) such that
A11: q = x and
A12: r > q /. 2 ;
q `2 < r by A12, JORDAN2B:29;
hence x in P ` by A7, A11; :: thesis: verum

end;

then A13: P ` = { p where p is Point of (TOP-REAL 2) : r > p /. 2 } by A8;
reconsider P1 = P ` as Subset of (TOP-REAL 2) ;
P1 is open by A2, A13, JORDAN2B:12;
hence P is closed by TOPS_1:3; :: thesis: verum