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