set U2 = the OSSubAlgebra of U1;
take the OSSubAlgebra of U1 ; :: thesis: the OSSubAlgebra of U1 is monotone
thus the OSSubAlgebra of U1 is monotone by Th14; :: thesis: verum