let U0 be Universal_Algebra; :: thesis: for U1 being SubAlgebra of U0 holds the carrier of U1 c= the carrier of U0
let U1 be SubAlgebra of U0; :: thesis: the carrier of U1 c= the carrier of U0
the carrier of U1 is Subset of U0 by UNIALG_2:def 7;
hence the carrier of U1 c= the carrier of U0 ; :: thesis: verum