theorem Th74: :: TOPS_5:74

for I being 2 -element set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for f being Function of (product J),[:(J . i),(J . j):] st i <> j & f = <:(proj (J,i)),(proj (J,j)):> holds
f is being_homeomorphism