for G being finite Group
for p being prime Nat st p divides card G holds
ex g being Element of G st ord g = p