set t2 = the Element of [.0,+infty.];
ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> the Element of [.0,+infty.] & q is_StoppingTime_wrt MyFunc,S ) by Th1;
hence ex b₁ being random_variable of Sigma, ExtBorelsubsets st b₁ is MyFunc -StoppingTime-like by Def11111; :: thesis: verum