:: deftheorem defines is_StoppingTime_wrt FINANCE4:def 5 :
for Omega being non empty set
for T being Nat
for MyFunc being Function
for k being Function of Omega,(StoppingSetExt T) holds
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w = t } in MyFunc . t );