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 }

A8: P ` c= { p where p is Point of (TOP-REAL 2) : r > p /. 2 }

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

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

{ p where p is Point of (TOP-REAL 2) : p `2 < r } c= P `
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;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

proof

then A7:
P ` = { p where p is Point of (TOP-REAL 2) : p `2 < r }
by A3;
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 ) ;

hence x in P ` by SUBSET_1:def 4; :: thesis: verum

end;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 }

then
x in the carrier of (TOP-REAL 2) \ P
by A1, A6, XBOOLE_0:def 5;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 ex q being Point of (TOP-REAL 2) st

( q = x & q `2 >= r ) ;

hence contradiction by A6; :: thesis: verum

hence x in P ` by SUBSET_1:def 4; :: thesis: verum

A8: P ` c= { p where p is Point of (TOP-REAL 2) : r > p /. 2 }

proof

{ p where p is Point of (TOP-REAL 2) : r > p /. 2 } c= P `
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;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

proof

then A13:
P ` = { p where p is Point of (TOP-REAL 2) : r > p /. 2 }
by A8;
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;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

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