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

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