let X be set ; :: thesis: ( X is finite implies ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n )
assume A1: X is finite ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n
defpred S₁[ set , set ] means ex k1, k2 being Element of NAT st
( $1 = k1 & $2 = k2 & k1 >= k2 );

now

per cases ( X /\ NAT = {} or X /\ NAT <> {} ) ;

suppose A3: X /\ NAT = {} ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n

thus ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n :: thesis: verum

proof

take 0 ; :: thesis: for k being Element of NAT st k in X holds
k <= 0
let k be Element of NAT ; :: thesis: ( k in X implies k <= 0 )
assume k in X ; :: thesis: k <= 0
hence k <= 0 by A3, XBOOLE_0:def 4; :: thesis: verum

end;

end;

suppose A5: X /\ NAT <> {} ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n

reconsider XN = X /\ NAT as finite set by A1;
A6: XN <> {} by A5;
A7: for x, y being set st S₁[x,y] & S₁[y,x] holds
x = y by XXREAL_0:1;
A8: for x, y, z being set st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by XXREAL_0:2;
consider x being set such that
A9: ( x in XN & ( for y being set st y in XN & y <> x holds
not S₁[y,x] ) ) from CARD_3:sch 2(A6, A7, A8);
reconsider n = x as Element of NAT by A9, XBOOLE_0:def 4;
take n = n; :: thesis: for k being Element of NAT st k in X holds
k <= n
let k be Element of NAT ; :: thesis: ( k in X implies k <= n )
assume k in X ; :: thesis: k <= n
then k in X /\ NAT by XBOOLE_0:def 4;
hence k <= n by A9; :: thesis: verum

end;

end;

end;

hence ex n being Element of NAT st
for k being Element of NAT st k in X holds
k <= n ; :: thesis: verum