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