defpred S1[ Point of (TOP-REAL 2)] means $1 `2 >= (2 * ($1 `1)) - 1;
reconsider L = { p where p is Point of (TOP-REAL 2) : S1[p] } as closed Subset of (TOP-REAL 2) by Th20;
defpred S2[ Point of (TOP-REAL 2)] means $1 `2 >= 1 - (2 * ($1 `1));
reconsider K = { p where p is Point of (TOP-REAL 2) : S2[p] } as closed Subset of (TOP-REAL 2) by Th22;
set T = { p where p is Point of (TOP-REAL 2) : ( S2[p] & S1[p] ) } ;
{ p where p is Point of (TOP-REAL 2) : ( S2[p] & S1[p] ) } = { p where p is Point of (TOP-REAL 2) : S2[p] } /\ { p where p is Point of (TOP-REAL 2) : S1[p] }
from DOMAIN_1:sch 10();
then
{ p where p is Point of (TOP-REAL 2) : ( S2[p] & S1[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)
; verum