let r be real number ; :: thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= 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 `1 <= r } implies P is closed )
assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } ; :: thesis: P is closed
A2: 1 in Seg 2 by FINSEQ_1:3;
A3: P ` = { p where p is Point of (TOP-REAL 2) : p `1 > r }

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `1 > r } )
assume A5: x in P ` ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : p `1 > r }
then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def 5;
then A6: ( x in the carrier of (TOP-REAL 2) & not x in P ) by XBOOLE_0:def 5;
reconsider q = x as Point of (TOP-REAL 2) by A5;
q `1 > r by A1, A6;
hence x in { p where p is Point of (TOP-REAL 2) : p `1 > r } ; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 > r } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : p `1 > r } ; :: thesis: x in P `
then consider p being Point of (TOP-REAL 2) such that
A7: ( p = x & p `1 > r ) ;

now

assume x in { q where q is Point of (TOP-REAL 2) : q `1 <= r } ; :: thesis: contradiction
then consider q being Point of (TOP-REAL 2) such that
A8: ( q = x & q `1 <= r ) ;
thus contradiction by A7, A8; :: thesis: verum

end;

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

end;

hence P ` = { p where p is Point of (TOP-REAL 2) : p `1 > r } by A4, XBOOLE_0:def 10; :: thesis: verum

end;

A9: P ` = { p where p is Point of (TOP-REAL 2) : r < Proj p,1 }

proof

A10: P ` c= { p where p is Point of (TOP-REAL 2) : r < Proj p,1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r < Proj p,1 } )
assume x in P ` ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : r < Proj p,1 }
then consider p being Point of (TOP-REAL 2) such that
A11: ( p = x & p `1 > r ) by A3;
Proj p,1 > r by A11, JORDAN2B:35;
hence x in { p where p is Point of (TOP-REAL 2) : r < Proj p,1 } by A11; :: thesis: verum

end;

{ p where p is Point of (TOP-REAL 2) : r < Proj p,1 } c= P `

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r < Proj p,1 } or x in P ` )
assume x in { p where p is Point of (TOP-REAL 2) : r < Proj p,1 } ; :: thesis: x in P `
then consider q being Point of (TOP-REAL 2) such that
A12: ( q = x & r < Proj q,1 ) ;
q `1 > r by A12, JORDAN2B:35;
hence x in P ` by A3, A12; :: thesis: verum

end;

hence P ` = { p where p is Point of (TOP-REAL 2) : r < Proj p,1 } by A10, XBOOLE_0:def 10; :: thesis: verum

end;

reconsider P1 = P ` as Subset of (TOP-REAL 2) ;
P1 is open by A2, A9, JORDAN2B:17;
hence P is closed by TOPS_1:29; :: thesis: verum