( 0 in StoppingSet T or 0 in {+infty} ) ;
then reconsider My1 = 0 as Element of StoppingSetExt T by XBOOLE_0:def 3;
Omega --> My1 is_StoppingTime_wrt MyFunc,T by FINANCE4:3;
hence ex b₁ being Function of Omega,(StoppingSetExt T) st b₁ is MyFunc -StoppingTime-like by Def1; :: thesis: verum