defpred S₁[ Point of ] means |.($1 - |[a,b]|).| >= r;
{ p where p is Point of : S₁[p] } c= the carrier of (TOP-REAL 2) from FRAENKEL:sch 10();
hence { p where p is Point of : |.(p - |[a,b]|).| >= r } is Subset of ; :: thesis: verum