for Omega being non empty set
for Sigma being SigmaField of Omega st Omega = {1,2,3,4} holds
for MyFunc being Filtration of StoppingSet 2,Sigma st MyFunc . 0 = Special_SigmaField1 & MyFunc . 1 = Special_SigmaField2 & MyFunc . 2 = Trivial-SigmaField Omega holds
ex ST being Function of Omega,(StoppingSetExt 2) st
( ST is_StoppingTime_wrt MyFunc,2 & ST . 1 = 1 & ST . 2 = 1 & ST . 3 = 2 & ST . 4 = 2 & { w where w is Element of Omega : ST . w = 0 } = {} & { w where w is Element of Omega : ST . w = 1 } = {1,2} & { w where w is Element of Omega : ST . w = 2 } = {3,4} )