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