theorem Th64: :: TOPS_5:64

for I being 1 -element set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product (Carrier J)) holds
( P in product_prebasis J iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )