:: deftheorem defines generating GROUP_4:def 5 :
for G being Group
for a being Element of G holds
( a is generating iff ex A being Subset of G st
( gr A = multMagma(# the carrier of G, the multF of G #) & not gr (A \ {a}) = multMagma(# the carrier of G, the multF of G #) ) );