consider U2 being OSSubAlgebra of U1;
take U2 ; :: thesis: U2 is monotone
thus U2 is monotone by Th15; :: thesis: verum