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

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