theorem Th21: :: PENCIL_3:21

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st B1 misses B2 holds
( B1 '||' B2 iff for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) )