set x = the strict OSSubAlgebra of U0;
the strict OSSubAlgebra of U0 in OSSub U0 by Def14;
hence not OSSub U0 is empty ; :: thesis: verum