8 * (0_ G) = 0_ G by Lm4;
hence not 0_ G is being_of_order_0 ; :: thesis: verum