for I being non empty set
for A being PLS-yielding ManySortedSet of I
for p, q being Point of (Segre_Product A) st p <> q holds
( p,q are_collinear iff for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) )