set R = the monotone OSCongruence of U1;
take the monotone OSCongruence of U1 ; :: thesis: the monotone OSCongruence of U1 is monotone
thus the monotone OSCongruence of U1 is monotone ; :: thesis: verum