let G be finite Group; :: thesis: ex g being Element of G st ord g = upper_bound (Ordset G)
set A = Ordset G;
set l = upper_bound (Ordset G);
( Ordset G <> {} & Ordset G c= REAL ) by NUMBERS:19, XBOOLE_1:1;
then upper_bound (Ordset G) in Ordset G by SEQ_4:133;
then consider g being Element of G such that
A3: ord g = upper_bound (Ordset G) ;
take g ; :: thesis: ord g = upper_bound (Ordset G)
thus ord g = upper_bound (Ordset G) by A3; :: thesis: verum