consider t2 being object such that

A0: t2 in I by XBOOLE_0:def 1;

reconsider t2 = t2 as Element of I by A0;

ex q being random_variable of Sigma, BorelSubsets I st

( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc ) by Th1;

hence ex b_{1} being random_variable of Sigma, BorelSubsets I st b_{1} is MyFunc -StoppingTime-like
by Def1111; :: thesis: verum

A0: t2 in I by XBOOLE_0:def 1;

reconsider t2 = t2 as Element of I by A0;

ex q being random_variable of Sigma, BorelSubsets I st

( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc ) by Th1;

hence ex b