:: deftheorem defines Special_StoppingSet FINANCE4:def 8 :
for t being object holds Special_StoppingSet t = IFIN (t,{1,2},1,2);