let I be non empty set ; :: thesis: 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
let A be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: ( ( 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 ) ) implies Segre_Product A is with_non_trivial_blocks )
assume A1: 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 ) ; :: thesis: Segre_Product A is with_non_trivial_blocks
for k being Block of (Segre_Product A) holds 2 c= card k

proof

let k be Block of (Segre_Product A); :: thesis: 2 c= card k
not Segre_Product A is void by A1, Th15;
then consider B being Segre-like ManySortedSubset of Carrier A such that
A2: k = product B and
A3: ex i being Element of I st B . i is Block of (A . i) by Def22;
consider i being Element of I such that
A4: B . i is Block of (A . i) by A3;
A . i is with_non_trivial_blocks by A1;
then 2 c= card (B . i) by A4;
then A5: not B . i is trivial by Th4;
dom B = I by PARTFUN1:def 2;
then B . i in rng B by FUNCT_1:def 3;
then reconsider BB = B as non trivial-yielding Segre-like ManySortedSet of I by A5, Def16;
not product BB is trivial ;
hence 2 c= card k by A2, Th4; :: thesis: verum

end;

hence Segre_Product A is with_non_trivial_blocks ; :: thesis: verum