theorem :: FINANCE3:2

for T being Element of NAT holds { w where w is Element of NAT : ( w > 0 & w <= T ) } c= { w where w is Element of NAT : w <= T }