defpred S₁[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 <= p `2 );
thus ex IT being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in IT iff S₁[x] ) from TOPREAL1:sch 2(); :: thesis: verum