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