for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for k1, k2 being StoppingTime_Func of MyFunc st k1 <= k2 holds
Sigma_tau k1 c= Sigma_tau k2