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

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