theorem :: OSALG_3:18

for S1 being OrderSortedSign
for U1, U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
( U1 is monotone iff U2 is monotone )