for G being finite Group ex g being Element of G st ord g = upper_bound (Ordset G)