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

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