:: deftheorem defines StoppingSetExt FINANCE4:def 3 :
for T being Nat holds StoppingSetExt T = (StoppingSet T) \/ {+infty};