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