let S1, S2, T1, T2 be complete LATTICE; :: thesis: ( S1,S2 are_isomorphic & T1,T2 are_isomorphic implies UPS (S2,T1), UPS (S1,T2) are_isomorphic )
given f being Function of S1,S2 such that A1: f is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: ( not T1,T2 are_isomorphic or UPS (S2,T1), UPS (S1,T2) are_isomorphic )
given g being Function of T1,T2 such that A2: g is isomorphic ; :: according to WAYBEL_1:def 8 :: thesis: UPS (S2,T1), UPS (S1,T2) are_isomorphic
take UPS (f,g) ; :: according to WAYBEL_1:def 8 :: thesis: UPS (f,g) is isomorphic
thus UPS (f,g) is isomorphic by A1, A2, Th35; :: thesis: verum