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

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