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