theorem :: FREEALG:1

for U0 being strict Universal_Algebra
for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds
( A is GeneratorSet of U0 iff GenUnivAlg A = U0 )