for S being OrderSortedSign
for U1 being non-empty OSAlgebra of S
for R being OSCongruence of U1 st R = [| the Sorts of U1, the Sorts of U1|] holds
R is monotone