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