for I being non empty set
for A being PLS-yielding ManySortedSet of I
for i being Element of I
for p being Point of (A . i)
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st i <> indx L holds
L +* (i,{p}) is non trivial-yielding Segre-like ManySortedSubset of Carrier A