let m be Element of NAT ; :: thesis: for X being finite Subset of [:NAT,{m}:] ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X
let X be finite Subset of [:NAT,{m}:]; :: thesis: ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X

per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X

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: for l being Element of NAT st l >= k holds
not [l,m] in X
let l be Element of NAT ; :: thesis: ( l >= k implies not [l,m] in X )
assume A2: l >= k ; :: thesis: not [l,m] in X
assume [l,m] in X ; :: thesis: contradiction
then A3: l in (Seg n) \/ {0} by A1, ZFMISC_1:87;

now :: thesis: contradiction

per cases ( l in Seg n or l in {0} ) by A3, XBOOLE_0:def 3;

suppose l in Seg n ; :: thesis: contradiction

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

end;

suppose l in {0} ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose X is empty ; :: thesis: ex k being Element of NAT st
for l being Element of NAT st l >= k holds
not [l,m] in X

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: verum

end;

end;