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 () st ( for G being finite Subset of F holds not [#] () 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 () st ( for G being finite Subset of F holds not [#] () 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 () st ( for G being finite Subset of F holds not [#] () 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 (); :: thesis: ( ( for G being finite Subset of F holds not [#] () 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 [#] () 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 ;
A <> [#] ()
proof
reconsider G1 = {A} as finite Subset of F by ;
assume A = [#] () ; :: thesis: contradiction
then union G1 = [#] () 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