defpred S₁[ Point of ] 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 : S₁[p] } c= the carrier of (TOP-REAL 2) from FRAENKEL:sch 10();
hence { p where p is Point of : ( not a <= p `1 or not p `1 <= b or not c <= p `2 or not p `2 <= d ) } is Subset of ; :: thesis: verum