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