:: deftheorem defines StoppingSet FINANCE4:def 2 :
for T being Nat holds StoppingSet T = { t where t is Element of NAT : ( 0 <= t & t <= T ) } ;