theorem LM202: :: GROUP_18:1

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