for S1 being OrderSortedSign
for U1, U2, U3 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic holds
U1,U3 are_os_isomorphic