let U1 be SubAlgebra of U0; :: thesis: U1 is with_const_op
reconsider U2 = U1 as Universal_Algebra ;
consider u being Element of Constants U2;
Constants U2 = Constants U0 by Th6;
then u in Constants U2 ;
then ex u1 being Element of U2 st
( u = u1 & ex o being operation of U2 st
( arity o = 0 & u1 in rng o ) ) ;
hence U1 is with_const_op by UNIALG_2:def 12; :: thesis: verum