let U0 be Universal_Algebra; :: thesis: for U1 being strict SubAlgebra of U0
for B being non empty Subset of U0 st B = the carrier of U1 holds
GenUnivAlg B = U1
let U1 be strict SubAlgebra of U0; :: thesis: for B being non empty Subset of U0 st B = the carrier of U1 holds
GenUnivAlg B = U1
let B be non empty Subset of U0; :: thesis: ( B = the carrier of U1 implies GenUnivAlg B = U1 )
set W = GenUnivAlg B;
assume A1: B = the carrier of U1 ; :: thesis: GenUnivAlg B = U1
then GenUnivAlg B is SubAlgebra of U1 by Def12;
then A2: the carrier of (GenUnivAlg B) is non empty Subset of U1 by Def7;
the carrier of U1 c= the carrier of (GenUnivAlg B) by A1, Def12;
then the carrier of U1 = the carrier of (GenUnivAlg B) by A2;
hence GenUnivAlg B = U1 by Th12; :: thesis: verum