let S, T be non empty TopSpace; :: thesis: [: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 ; :: according to T_0TOPSP:def 1 :: thesis: f is being_homeomorphism
thus f is being_homeomorphism by Th43; :: thesis: verum