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₁ being random_variable of Sigma, BorelSubsets I st b₁ is MyFunc -StoppingTime-like by Def1111; :: thesis: verum