:: deftheorem defines '||' PENCIL_3:def 2 :
for I being non empty set
for A being PLS-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A holds
( B1 '||' B2 iff for x being Point of (Segre_Product A) st x in B1 holds
ex y being Point of (Segre_Product A) st
( y in B2 & x,y are_collinear ) );