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

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