let G be addGroup; :: thesis: ord (0_ G) = 1
A1: for n being Nat st n * (0_ G) = 0_ G & n <> 0 holds
1 <= n by NAT_1:14;
( not 0_ G is being_of_order_0 & 1 * (0_ G) = 0_ G ) by Lm4;
hence ord (0_ G) = 1 by A1, Def11; :: thesis: verum