let U0 be strict Universal_Algebra; :: thesis: for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds
( A is GeneratorSet of U0 iff GenUnivAlg A = U0 )
let A be Subset of U0; :: thesis: ( ( Constants U0 <> {} or A <> {} ) implies ( A is GeneratorSet of U0 iff GenUnivAlg A = U0 ) )
assume A1: ( Constants U0 <> {} or A <> {} ) ; :: thesis: ( A is GeneratorSet of U0 iff GenUnivAlg A = U0 )
thus ( A is GeneratorSet of U0 implies GenUnivAlg A = U0 ) :: thesis: ( GenUnivAlg A = U0 implies A is GeneratorSet of U0 )
proof
assume A is GeneratorSet of U0 ; :: thesis: GenUnivAlg A = U0
then A2: the carrier of (GenUnivAlg A) = the carrier of U0 by A1, Lm3;
U0 is strict SubAlgebra of U0 by UNIALG_2:8;
hence GenUnivAlg A = U0 by A2, UNIALG_2:12; :: thesis: verum
end;
assume GenUnivAlg A = U0 ; :: thesis: A is GeneratorSet of U0
hence A is GeneratorSet of U0 by A1, Lm3; :: thesis: verum