for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds
Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)