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