:: deftheorem defines is_StoppingTime_wrt FINANCE4:def 4 :
for T being Nat
for F being Function
for R being Relation holds
( R is_StoppingTime_wrt F,T iff for t being Element of StoppingSet T holds Coim (R,t) in F . t );