consider x being strict OSSubAlgebra of U0;
x in OSSub U0 by Def15;
hence not OSSub U0 is empty ; :: thesis: verum