:: deftheorem defines Generators AOFA_000:def 9 :
for A being Universal_Algebra holds Generators A = the carrier of A \ (union { (rng o) where o is Element of Operations A : verum } );