for A being Universal_Algebra
for G being Subset of A holds
( G is GeneratorSet of A iff for I being Element of A ex n being Nat st I in G |^ n )