for I being non empty set
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 A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )