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