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 t2 being Element of [.0,+infty.] ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S )