for T being Nat st T > 0 holds
{ w where w is Element of NAT : ( w > 0 & w <= T ) } is non empty Subset of NAT