for S, T being non empty TopSpace
for f being Function of [:S,T:],[:T,S:] st f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> holds
f is being_homeomorphism