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