theorem Th23: :: OSALG_4:23

for S being OrderSortedSign
for U1 being non-empty monotone OSAlgebra of S
for R being OSCongruence of U1 holds R is monotone