defpred S₁[ Point of (TOP-REAL 2)] means $1 `2 >= 1 - (2 * ($1 `1 ));
defpred S₂[ Point of (TOP-REAL 2)] means $1 `2 >= (2 * ($1 `1 )) - 1;
set T = { p where p is Point of (TOP-REAL 2) : ( S₁[p] & S₂[p] ) } ;
reconsider K = { p where p is Point of (TOP-REAL 2) : S₁[p] } as closed Subset of (TOP-REAL 2) by Th22;
reconsider L = { p where p is Point of (TOP-REAL 2) : S₂[p] } as closed Subset of (TOP-REAL 2) by Th20;
{ p where p is Point of (TOP-REAL 2) : ( S₁[p] & S₂[p] ) } = { p where p is Point of (TOP-REAL 2) : S₁[p] } /\ { p where p is Point of (TOP-REAL 2) : S₂[p] } from DOMAIN_1:sch 10();
then { p where p is Point of (TOP-REAL 2) : ( S₁[p] & S₂[p] ) } = K /\ L ;
hence { p where p is Point of (TOP-REAL 2) : ( p `2 >= 1 - (2 * (p `1 )) & p `2 >= (2 * (p `1 )) - 1 ) } is closed Subset of (TOP-REAL 2) by TOPS_1:35; :: thesis: verum