for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) holds
( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )