let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr of 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 of 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 A1: A is opers_closed ; :: thesis: the carrier of (GenAlg A) = A
A2: A c= the carrier of (GenAlg A) by Def5;
consider C being strict Subalgebra of B such that
A3: the carrier of C = A by A1, Th20;
the carrier of (GenAlg A) c= A by A3, Def5;
hence the carrier of (GenAlg A) = A by A2, XBOOLE_0:def 10; :: thesis: verum