let m be Element of NAT ; :: thesis:
let X be finite Subset of [:NAT,{m}:]; :: thesis:

per cases ;

suppose not X is empty ; :: thesis:

then reconsider X9 = X as non empty finite Subset of [:NAT,{m}:] ;
consider n being non zero Element of NAT such that
A1: X9 c= [:((Seg n) \/ {0}),{m}:] by Th3;
take k = n + 1; :: thesis:
let l be Element of NAT ; :: thesis:
assume A2: l >= k ; :: thesis:
assume [l,m] in X ; :: thesis:
then A3: l in (Seg n) \/ {0} by A1, ZFMISC_1:87;

now :: thesis:

per cases by A3, XBOOLE_0:def 3;

suppose l in Seg n ; :: thesis:

then l <= n by FINSEQ_1:1;
hence contradiction by A2, NAT_1:13; :: thesis:

end;

suppose l in {0} ; :: thesis:

hence contradiction by A2, TARSKI:def 1; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

suppose X is empty ; :: thesis:

then for l being Element of NAT st l >= 0 holds
not [l,m] in X ;
hence ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X ; :: thesis:

end;

end;