let Omega be non empty set ; for Sigma being SigmaField of Omega
for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let Sigma be SigmaField of Omega; for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let T be Nat; for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let MyFunc be Filtration of StoppingSet T,Sigma; for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
let k1, k2 be Function of Omega,(StoppingSetExt T); ( k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T implies ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) )
assume ASS:
( k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T )
; ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
set k3 = max (k1,k2);
max (k1,k2) is Function of Omega,(StoppingSetExt T)
then reconsider k3 = max (k1,k2) as Function of Omega,(StoppingSetExt T) ;
k3 is_StoppingTime_wrt MyFunc,T
hence
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
; verum