:: deftheorem Def11 defines ord GROUP_1:def 11 :
for G being Group
for h being Element of G
for b₃ being Element of NAT holds
( ( h is being_of_order_0 implies ( b₃ = ord h iff b₃ = 0 ) ) & ( not h is being_of_order_0 implies ( b₃ = ord h iff ( h |^ b₃ = 1_ G & b₃ <> 0 & ( for m being Nat st h |^ m = 1_ G & m <> 0 holds
b₃ <= m ) ) ) ) );