for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I
for x being Point of (Segre_Product A) holds x is ManySortedSet of I