(1_ G) |^ 8 = 1_ G by Lm4;
hence not 1_ G is being_of_order_0 ; :: thesis: verum