let X be set ; :: thesis:
assume A1: X is finite ; :: thesis:
defpred S₁[ object , object ] means ex k1, k2 being Nat st
( $1 = k1 & $2 = k2 & k1 >= k2 );

now :: thesis:

per cases ;

suppose A2: X /\ NAT = {} ; :: thesis:

thus ex n being Nat st
for k being Nat st k in X holds
k <= n :: thesis:

proof

take 0 ; :: thesis:
let k be Nat; :: thesis:
A3: k in NAT by ORDINAL1:def 12;
assume k in X ; :: thesis:
hence k <= 0 by A2, XBOOLE_0:def 4, A3; :: thesis:

end;

end;

suppose A4: X /\ NAT <> {} ; :: thesis:

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

end;

end;

end;

hence ex n being Nat st
for k being Nat st k in X holds
k <= n ; :: thesis: