theorem Th17: :: PENCIL_1:17

for I being non empty set
for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds
( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is with_non_trivial_blocks