:: deftheorem defines vertical SPPOL_1:def 3 :
for P being Subset of (TOP-REAL 2) holds
( P is vertical iff for p, q being Point of (TOP-REAL 2) st p in P & q in P holds
p `1 = q `1 );