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

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 5 :: thesis: the carrier of (GenUnivAlg G) = the carrier of A
reconsider C = the carrier of (GenUnivAlg G) as non empty Subset of A by UNIALG_2:def 8;
A3: G c= C by A1, UNIALG_2:def 13;
C is opers_closed by UNIALG_2:def 8;
hence the carrier of (GenUnivAlg G) = the carrier of A by A2, A3; :: thesis: verum

end;

assume A4: 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 5 :: thesis: ( B is opers_closed & G c= B implies B = the carrier of A )
assume A5: ( B is opers_closed & G c= B ) ; :: thesis: B = the carrier of A
thus B c= the carrier of A ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of A c= B
reconsider C = B as non empty Subset of A by A1, A5, Lm2, XBOOLE_1:3;
A6: UniAlgSetClosed C = UAStr(# C,(Opers A,C) #) by A5, UNIALG_2:def 9;
then GenUnivAlg G is SubAlgebra of UniAlgSetClosed C by A1, A5, UNIALG_2:def 13;
then the carrier of A is Subset of C by A4, A6, UNIALG_2:def 8;
hence the carrier of A c= B ; :: thesis: verum