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