theorem :: GROUP_1A:39

for G being addGroup holds ord (0_ G) = 1