let I be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of () st ( for G being finite Subset of F holds not [#] () c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis: for i being Element of I
for F being Subset of () st ( for G being finite Subset of F holds not [#] () c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

let i be Element of I; :: thesis: for F being Subset of () st ( for G being finite Subset of F holds not [#] () c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

let F be Subset of (); :: thesis: ( ( for G being finite Subset of F holds not [#] () c= union G ) implies for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A ) )

assume A1: for G being finite Subset of F holds not [#] () c= union G ; :: thesis: for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

let xi be Element of (J . i); :: thesis: for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

let G be finite Subset of F; :: thesis: ( (proj (J,i)) " {xi} c= union G implies ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A ) )

reconsider G9 = G as Subset of () by XBOOLE_1:1;
assume A2: (proj (J,i)) " {xi} c= union G ; :: thesis: ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )

assume for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ; :: thesis: contradiction
then [#] () c= union G9 by ;
hence contradiction by A1; :: thesis: verum