let a be Element of G; :: thesis: a is p -element
consider m being natural number such that
A1: card G = p |^ m by GROUP_10:def 17;
ex r being natural number st
( ord a = p |^ r & r <= m ) by A1, GR_CY_1:28, Th2;
hence a is p -element by def1; :: thesis: verum