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