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