theorem :: TOPS_5:75

for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I st i <> j holds
product J,[:(J . i),(J . j):] are_homeomorphic