for m being Element of NAT
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