defpred S_{1}[ Point of (TOP-REAL 2)] means ( a <= $1 `1 & $1 `1 <= b & c <= $1 `2 & $1 `2 <= d );

{ p where p is Point of (TOP-REAL 2) : S_{1}[p] } c= the carrier of (TOP-REAL 2)
from FRAENKEL:sch 10();

hence { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } is Subset of (TOP-REAL 2) ; :: thesis: verum

{ p where p is Point of (TOP-REAL 2) : S

hence { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } is Subset of (TOP-REAL 2) ; :: thesis: verum