theorem :: FINANCE4:3

for Omega being non empty set
for Sigma being SigmaField of Omega
for T being Nat
for TFix being Element of StoppingSetExt T
for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T