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