theorem Th56: :: TOPS_5:56

for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I holds {} in product_prebasis J