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