let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
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 TopSpace-yielding ManySortedSet of ; :: 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 G' = 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 G' by A2, Th20;
hence contradiction by A1; :: thesis: verum