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 Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
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 Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
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 Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
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 Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )
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 Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
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 Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
let G be finite Subset of F; :: thesis: ( (proj (J,i)) " {xi} c= union G implies ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open ) )
assume (proj (J,i)) " {xi} c= union G ; :: thesis: ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
then consider A being set such that
A2: A in product_prebasis J and
A3: A in G and
A4: (proj (J,i)) " {xi} c= A by A1, Th20;
A <> [#] (product J)

proof

reconsider G1 = {A} as finite Subset of F by A3, ZFMISC_1:31;
assume A = [#] (product J) ; :: thesis: contradiction
then union G1 = [#] (product J) by ZFMISC_1:25;
hence contradiction by A1; :: thesis: verum

end;

then consider Ai being Subset of (J . i) such that
A5: Ai <> [#] (J . i) and
A6: xi in Ai and
A7: Ai is open and
A8: A = (proj (J,i)) " Ai by A2, A4, Th17;
take Ai ; :: thesis: ( Ai <> [#] (J . i) & xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
thus Ai <> [#] (J . i) by A5; :: thesis: ( xi in Ai & (proj (J,i)) " Ai in G & Ai is open )
thus xi in Ai by A6; :: thesis: ( (proj (J,i)) " Ai in G & Ai is open )
thus (proj (J,i)) " Ai in G by A3, A8; :: thesis: Ai is open
thus Ai is open by A7; :: thesis: verum