consider R being monotone OSCongruence of U1;
take R ; :: thesis: R is monotone
thus R is monotone ; :: thesis: verum