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