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