theorem Th58: :: TOPS_5:58

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