theorem Th65: :: TOPS_5:65

for I being 1 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I holds the topology of (product J) = product_prebasis J