:: deftheorem defines being_of_order_0 GROUP_1:def 10 :
for G being Group
for h being Element of G holds
( h is being_of_order_0 iff for n being Nat st h |^ n = 1_ G holds
n = 0 );