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 identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds
Segre_Product A is identifying_close_blocks