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 t2 being Element of I ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )