for S1, S2, T1, T2 being complete LATTICE st S1,S2 are_isomorphic & T1,T2 are_isomorphic holds
UPS (S2,T1), UPS (S1,T2) are_isomorphic