theorem Th69: :: TOPS_5:69

for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product (Carrier J)) st i <> j holds
( P in product_prebasis J iff ( ex V being Subset of (J . i) st
( V is open & P = product ((i,j) --> (V,([#] (J . j)))) ) or ex W being Subset of (J . j) st
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) ) ) )