( 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_{1} being Function of Omega,(StoppingSetExt T) st b_{1} is MyFunc -StoppingTime-like
by Def1; :: thesis: verum

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