defpred S₁[ Point of (TOP-REAL 2)] means ( not a < $1 `1 or not $1 `1 < b or not c < $1 `2 or not $1 `2 < d );
{ 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) : ( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) } is Subset of (TOP-REAL 2) ; :: thesis: verum