let G be finite Group; :: thesis: for a being Element of G holds ord a divides card G
let a be Element of G; :: thesis: ord a divides card G
ord a = card (gr {a}) by Th7;
hence ord a divides card G by GROUP_2:148; :: thesis: verum