let I be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for F being Subset of st ( for G being finite Subset of holds not [#] (product J) c= union G ) holds
for xi being Element of
for G being finite Subset of 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 I; :: thesis: for i being Element of I
for F being Subset of st ( for G being finite Subset of holds not [#] (product J) c= union G ) holds
for xi being Element of
for G being finite Subset of 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 holds not [#] (product J) c= union G ) holds
for xi being Element of
for G being finite Subset of 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 holds not [#] (product J) c= union G ) implies for xi being Element of
for G being finite Subset of 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 holds not [#] (product J) c= union G ; :: thesis: for xi being Element of
for G being finite Subset of 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 ; :: thesis: for G being finite Subset of 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 ; :: 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 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