let A be Universal_Algebra; :: thesis: for B being Subset of A st ( B <> {} or Constants A <> {} ) holds
( B is GeneratorSet of A iff the carrier of (GenUnivAlg B) = the carrier of A )
let G be Subset of A; :: thesis: ( ( G <> {} or Constants A <> {} ) implies ( G is GeneratorSet of A iff the carrier of (GenUnivAlg G) = the carrier of A ) )
assume A1: ( G <> {} or Constants A <> {} ) ; :: thesis: ( G is GeneratorSet of A iff the carrier of (GenUnivAlg G) = the carrier of A )
thus ( G is GeneratorSet of A implies the carrier of (GenUnivAlg G) = the carrier of A ) :: thesis: ( the carrier of (GenUnivAlg G) = the carrier of A implies G is GeneratorSet of A )
proof
reconsider C = the carrier of (GenUnivAlg G) as non empty Subset of A by UNIALG_2:def 7;
assume A2: for B being Subset of A st B is opers_closed & G c= B holds
B = the carrier of A ; :: according to FREEALG:def 4 :: thesis: the carrier of (GenUnivAlg G) = the carrier of A
( G c= C & C is opers_closed ) by UNIALG_2:def 7, UNIALG_2:def 12;
hence the carrier of (GenUnivAlg G) = the carrier of A by A2; :: thesis: verum
end;
assume A3: the carrier of (GenUnivAlg G) = the carrier of A ; :: thesis: G is GeneratorSet of A
let B be Subset of A; :: according to FREEALG:def 4 :: thesis: ( B is opers_closed & G c= B implies B = the carrier of A )
assume that
A4: B is opers_closed and
A5: G c= B ; :: thesis: B = the carrier of A
reconsider C = B as non empty Subset of A by A1, A4, A5, Lm2, XBOOLE_1:3;
thus B c= the carrier of A ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of A c= B
A6: UniAlgSetClosed C = UAStr(# C,(Opers (A,C)) #) by A4, UNIALG_2:def 8;
then GenUnivAlg G is SubAlgebra of UniAlgSetClosed C by A1, A5, UNIALG_2:def 12;
then the carrier of A is Subset of C by A3, A6, UNIALG_2:def 7;
hence the carrier of A c= B ; :: thesis: verum