theorem Th19: :: YELLOW17:19

for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for G being Subset of (product_prebasis J) st (proj (J,i)) " {xi} c= union G & ( for A being set st A in product_prebasis J & A in G holds
not (proj (J,i)) " {xi} c= A ) holds
[#] (product J) c= union G