let S, T be non empty TopSpace; [:S,T:],[:T,S:] are_homeomorphic
reconsider f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> as Function of [:S,T:],[:T,S:] by Th42;
take
f
; T_0TOPSP:def 1 f is being_homeomorphism
thus
f is being_homeomorphism
by Th43; verum