:: deftheorem defines StoppingSetExt FINANCE4:def 1 :
for I being ext-real-membered set holds StoppingSetExt I = I \/ {+infty};