:: deftheorem defines being_of_order_0 GROUP_1A:def 9 :
for G being addGroup
for h being Element of G holds
( h is being_of_order_0 iff for n being Nat st n * h = 0_ G holds
n = 0 );