for G being finite Group
for a being Element of G holds not a is being_of_order_0