let U0 be Universal_Algebra; :: thesis: for U1, U2 being strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds
U1 = U2
let U1, U2 be strict SubAlgebra of U0; :: thesis: ( the carrier of U1 = the carrier of U2 implies U1 = U2 )
assume the carrier of U1 = the carrier of U2 ; :: thesis: U1 = U2
then ( U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 ) by Th11;
hence U1 = U2 by Th10; :: thesis: verum