theorem Th30: :: AOFA_000:30

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 )