for T being Nat holds { w where w is Element of NAT : w <= T } is non empty Subset of NAT