theorem Th16: :: SPPOL_1:16

for p, q being Point of (TOP-REAL 2) holds
( p `1 = q `1 iff LSeg (p,q) is vertical )