reconsider R = [|the Sorts of U1,the Sorts of U1|] as OSCongruence of U1 by Th21;
take R ; :: thesis: R is monotone
thus R is monotone by Th22; :: thesis: verum