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