for Omega being non empty set
for Sigma being SigmaField of Omega
for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )