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 (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) 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 (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) 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 (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) 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 (product_prebasis J); :: thesis: ( ( for G being finite Subset of F holds not [#] (product J) 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 [#] (product J) 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 (product_prebasis J) 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 [#] (product J) c= union G9 by A2, Th19;
hence contradiction by A1; :: thesis: verum