let N be Subset of NAT; :: thesis: ( N is finite implies ex k being Nat st
for n being Nat st n in N holds
n <= k )
assume N is finite ; :: thesis: ex k being Nat st
for n being Nat st n in N holds
n <= k
then reconsider n = card N as Nat ;
A1: N,n are_equipotent by CARD_1:def 2;
consider F being Function such that
F is one-to-one and
A2: dom F = n and
A3: rng F = N by A1, WELLORD2:def 4;
reconsider F = F as XFinSequence by A2, AFINSQ_1:5;
reconsider F = F as XFinSequence of NAT by A3, RELAT_1:def 19;
reconsider k = Sum F as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: for n being Nat st n in N holds
n <= k
let n be Nat; :: thesis: ( n in N implies n <= k )
assume A4: n in N ; :: thesis: n <= k
F <> 0 by A3, A4;
then A5: len F > 0 ;
ex x being object st
( x in dom F & F . x = n ) by A3, A4, FUNCT_1:def 3;
hence n <= k by A5, AFINSQ_2:61; :: thesis: verum