let I be non empty set ; :: thesis:
let J be non-Empty TopStruct-yielding ManySortedSet of I; :: thesis:
let i be Element of I; :: thesis:
let F be Subset of (product_prebasis J); :: thesis:
assume A1: for G being finite Subset of F holds not [#] (product J) c= union G ; :: thesis:
let xi be Element of (J . i); :: thesis:
let G be finite Subset of F; :: thesis:
assume (proj (J,i)) " {xi} c= union G ; :: thesis:
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)

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

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:
thus Ai <> [#] (J . i) by A5; :: thesis:
thus xi in Ai by A6; :: thesis:
thus (proj (J,i)) " Ai in G by A3, A8; :: thesis:
thus Ai is open by A7; :: thesis: