let U0 be with_const_op Universal_Algebra; :: thesis: for U1 being SubAlgebra of U0
for a being set st a is Element of Constants U0 holds
a in the carrier of U1
let U1 be SubAlgebra of U0; :: thesis: for a being set st a is Element of Constants U0 holds
a in the carrier of U1
let a be set ; :: thesis: ( a is Element of Constants U0 implies a in the carrier of U1 )
A1: Constants U0 is Subset of U1 by UNIALG_2:15;
assume a is Element of Constants U0 ; :: thesis: a in the carrier of U1
hence a in the carrier of U1 by A1, TARSKI:def 3; :: thesis: verum