let A be Universal_Algebra; 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; ( ( 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 <> {} )
; ( 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 )
( the carrier of (GenUnivAlg G) = the carrier of A implies G is GeneratorSet of A )
assume A3:
the carrier of (GenUnivAlg G) = the carrier of A
; G is GeneratorSet of A
let B be Subset of A; FREEALG:def 4 ( 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
; 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
; XBOOLE_0:def 10 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
; verum