:: deftheorem Def11 defines ord GROUP_1A:def 10 :
for G being addGroup
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 ( b₃ * h = 0_ G & b₃ <> 0 & ( for m being Nat st m * h = 0_ G & m <> 0 holds
b₃ <= m ) ) ) ) );