theorem :: TOPS_5:66

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