let G be finite Group; :: thesis: for x being Element of G holds
( 0 < ord x & ord x <= card G )
let x be Element of G; :: thesis: ( 0 < ord x & ord x <= card G )
not x is being_of_order_0 by GR_CY_1:6;
then 0 <> ord x by GROUP_1:def 11;
hence 0 < ord x ; :: thesis: ord x <= card G
ord x divides card G by GR_CY_1:8;
hence ord x <= card G by NAT_D:7; :: thesis: verum