let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr over L

for A being non empty Subset of B st A is opers_closed holds

the carrier of (GenAlg A) = A

let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subset of B st A is opers_closed holds

the carrier of (GenAlg A) = A

let A be non empty Subset of B; :: thesis: ( A is opers_closed implies the carrier of (GenAlg A) = A )

assume A is opers_closed ; :: thesis: the carrier of (GenAlg A) = A

then ex C being strict Subalgebra of B st the carrier of C = A by Th19;

then A1: the carrier of (GenAlg A) c= A by Def5;

A c= the carrier of (GenAlg A) by Def5;

hence the carrier of (GenAlg A) = A by A1, XBOOLE_0:def 10; :: thesis: verum

for A being non empty Subset of B st A is opers_closed holds

the carrier of (GenAlg A) = A

let B be non empty AlgebraStr over L; :: thesis: for A being non empty Subset of B st A is opers_closed holds

the carrier of (GenAlg A) = A

let A be non empty Subset of B; :: thesis: ( A is opers_closed implies the carrier of (GenAlg A) = A )

assume A is opers_closed ; :: thesis: the carrier of (GenAlg A) = A

then ex C being strict Subalgebra of B st the carrier of C = A by Th19;

then A1: the carrier of (GenAlg A) c= A by Def5;

A c= the carrier of (GenAlg A) by Def5;

hence the carrier of (GenAlg A) = A by A1, XBOOLE_0:def 10; :: thesis: verum