let Omega be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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)

k3 is_StoppingTime_wrt MyFunc,T

( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) ; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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)

proof

then reconsider k3 = max (k1,k2) as Function of Omega,(StoppingSetExt T) ;
rng (max (k1,k2)) c= StoppingSetExt T

hence max (k1,k2) is Function of Omega,(StoppingSetExt T) by FUNCT_2:def 1; :: thesis: verum

end;proof

then
max (k1,k2) is Function of (dom (max (k1,k2))),(StoppingSetExt T)
by FUNCT_2:2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (max (k1,k2)) or x in StoppingSetExt T )

assume x in rng (max (k1,k2)) ; :: thesis: x in StoppingSetExt T

then consider x2 being object such that

C1: ( x2 in dom (max (k1,k2)) & x = (max (k1,k2)) . x2 ) by FUNCT_1:def 3;

O1: x2 in Omega by C1;

x2 in dom k1 by O1, FUNCT_2:def 1;

then ZW1: k1 . x2 in rng k1 by FUNCT_1:3;

x2 in dom k2 by O1, FUNCT_2:def 1;

then ZW2: k2 . x2 in rng k2 by FUNCT_1:3;

max ((k1 . x2),(k2 . x2)) in StoppingSetExt T

end;assume x in rng (max (k1,k2)) ; :: thesis: x in StoppingSetExt T

then consider x2 being object such that

C1: ( x2 in dom (max (k1,k2)) & x = (max (k1,k2)) . x2 ) by FUNCT_1:def 3;

O1: x2 in Omega by C1;

x2 in dom k1 by O1, FUNCT_2:def 1;

then ZW1: k1 . x2 in rng k1 by FUNCT_1:3;

x2 in dom k2 by O1, FUNCT_2:def 1;

then ZW2: k2 . x2 in rng k2 by FUNCT_1:3;

max ((k1 . x2),(k2 . x2)) in StoppingSetExt T

proof
end;

hence
x in StoppingSetExt T
by Def20, C1; :: thesis: verumper cases
( k2 . x2 <= k1 . x2 or not k2 . x2 <= k1 . x2 )
;

end;

suppose
k2 . x2 <= k1 . x2
; :: thesis: max ((k1 . x2),(k2 . x2)) in StoppingSetExt T

then
k1 . x2 = max ((k1 . x2),(k2 . x2))
by XXREAL_0:def 10;

hence max ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW1; :: thesis: verum

end;hence max ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW1; :: thesis: verum

suppose
not k2 . x2 <= k1 . x2
; :: thesis: max ((k1 . x2),(k2 . x2)) in StoppingSetExt T

then
k2 . x2 = max ((k1 . x2),(k2 . x2))
by XXREAL_0:def 10;

hence max ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW2; :: thesis: verum

end;hence max ((k1 . x2),(k2 . x2)) in StoppingSetExt T by ZW2; :: thesis: verum

hence max (k1,k2) is Function of Omega,(StoppingSetExt T) by FUNCT_2:def 1; :: thesis: verum

k3 is_StoppingTime_wrt MyFunc,T

proof

hence
ex k3 being Function of Omega,(StoppingSetExt T) st
for t being Element of StoppingSet T holds { w where w is Element of Omega : k3 . w <= t } in MyFunc . t

end;proof

hence
k3 is_StoppingTime_wrt MyFunc,T
by KJK; :: thesis: verum
let t be Element of StoppingSet T; :: thesis: { w where w is Element of Omega : k3 . w <= t } in MyFunc . t

O1: { w where w is Element of Omega : k3 . w <= t } = { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }

end;O1: { w where w is Element of Omega : k3 . w <= t } = { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }

proof

O2:
{ w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } = { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t }
for x being object holds

( x in { w where w is Element of Omega : k3 . w <= t } iff x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } )

end;( x in { w where w is Element of Omega : k3 . w <= t } iff x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } )

proof

hence
{ w where w is Element of Omega : k3 . w <= t } = { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { w where w is Element of Omega : k3 . w <= t } iff x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } )

thus ( x in { w where w is Element of Omega : k3 . w <= t } implies x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } ) :: thesis: ( x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } implies x in { w where w is Element of Omega : k3 . w <= t } )

then consider w2 being Element of Omega such that

R1: ( x = w2 & k2 . w2 <= t & k1 . w2 <= t ) ;

HHH: k3 . w2 = max ((k1 . w2),(k2 . w2)) by Def20;

k3 . w2 <= t by HHH, XXREAL_0:def 10, R1;

hence x in { w where w is Element of Omega : k3 . w <= t } by R1; :: thesis: verum

end;thus ( x in { w where w is Element of Omega : k3 . w <= t } implies x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } ) :: thesis: ( x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } implies x in { w where w is Element of Omega : k3 . w <= t } )

proof

assume
x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }
; :: thesis: x in { w where w is Element of Omega : k3 . w <= t }
assume
x in { w where w is Element of Omega : k3 . w <= t }
; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }

then consider w2 being Element of Omega such that

R1: ( x = w2 & k3 . w2 <= t ) ;

HHH: k3 . w2 = max ((k1 . w2),(k2 . w2)) by Def20;

set K3 = k3 . w2;

set K1 = k1 . w2;

set K2 = k2 . w2;

end;then consider w2 being Element of Omega such that

R1: ( x = w2 & k3 . w2 <= t ) ;

HHH: k3 . w2 = max ((k1 . w2),(k2 . w2)) by Def20;

set K3 = k3 . w2;

set K1 = k1 . w2;

set K2 = k2 . w2;

per cases
( k1 . w2 <= k2 . w2 or k1 . w2 > k2 . w2 )
;

end;

suppose S1:
k1 . w2 <= k2 . w2
; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }

then
k3 . w2 = k2 . w2
by HHH, XXREAL_0:def 10;

then ( k2 . w2 <= t & k1 . w2 <= t ) by XXREAL_0:2, S1, R1;

hence x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } by R1; :: thesis: verum

end;then ( k2 . w2 <= t & k1 . w2 <= t ) by XXREAL_0:2, S1, R1;

hence x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } by R1; :: thesis: verum

suppose S1:
k1 . w2 > k2 . w2
; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }

then
k3 . w2 = k1 . w2
by HHH, XXREAL_0:def 10;

then ( k2 . w2 <= t & k1 . w2 <= t ) by XXREAL_0:2, S1, R1;

hence x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } by R1; :: thesis: verum

end;then ( k2 . w2 <= t & k1 . w2 <= t ) by XXREAL_0:2, S1, R1;

hence x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } by R1; :: thesis: verum

then consider w2 being Element of Omega such that

R1: ( x = w2 & k2 . w2 <= t & k1 . w2 <= t ) ;

HHH: k3 . w2 = max ((k1 . w2),(k2 . w2)) by Def20;

k3 . w2 <= t by HHH, XXREAL_0:def 10, R1;

hence x in { w where w is Element of Omega : k3 . w <= t } by R1; :: thesis: verum

proof

{ w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } in MyFunc . t
for x being object holds

( x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } iff x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } )

end;( x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } iff x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } )

proof

hence
{ w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } = { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t }
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } iff x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } )

thus ( x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } implies x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } ) :: thesis: ( x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } implies x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } )

then V0: ( x in { w where w is Element of Omega : k2 . w <= t } & x in { w where w is Element of Omega : k1 . w <= t } ) by XBOOLE_0:def 4;

consider w3 being Element of Omega such that

V1: ( x = w3 & k2 . w3 <= t ) by V0;

consider w3 being Element of Omega such that

V2: ( x = w3 & k1 . w3 <= t ) by V0;

thus x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } by V1, V2; :: thesis: verum

end;thus ( x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } implies x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } ) :: thesis: ( x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } implies x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } )

proof

assume
x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t }
; :: thesis: x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }
assume
x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) }
; :: thesis: x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t }

then consider w3 being Element of Omega such that

V2: ( x = w3 & k2 . w3 <= t & k1 . w3 <= t ) ;

V3: x in { w where w is Element of Omega : k2 . w <= t } by V2;

x in { w where w is Element of Omega : k1 . w <= t } by V2;

hence x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } by V3, XBOOLE_0:def 4; :: thesis: verum

end;then consider w3 being Element of Omega such that

V2: ( x = w3 & k2 . w3 <= t & k1 . w3 <= t ) ;

V3: x in { w where w is Element of Omega : k2 . w <= t } by V2;

x in { w where w is Element of Omega : k1 . w <= t } by V2;

hence x in { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } by V3, XBOOLE_0:def 4; :: thesis: verum

then V0: ( x in { w where w is Element of Omega : k2 . w <= t } & x in { w where w is Element of Omega : k1 . w <= t } ) by XBOOLE_0:def 4;

consider w3 being Element of Omega such that

V1: ( x = w3 & k2 . w3 <= t ) by V0;

consider w3 being Element of Omega such that

V2: ( x = w3 & k1 . w3 <= t ) by V0;

thus x in { w where w is Element of Omega : ( k2 . w <= t & k1 . w <= t ) } by V1, V2; :: thesis: verum

proof

hence
{ w where w is Element of Omega : k3 . w <= t } in MyFunc . t
by O2, O1; :: thesis: verum
reconsider M = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;

( { w where w is Element of Omega : k1 . w <= t } is Event of M & { w where w is Element of Omega : k2 . w <= t } is Event of M ) by ASS, KJK;

then { w where w is Element of Omega : k1 . w <= t } /\ { w where w is Element of Omega : k2 . w <= t } is Event of M by PROB_1:19;

hence { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } in MyFunc . t ; :: thesis: verum

end;( { w where w is Element of Omega : k1 . w <= t } is Event of M & { w where w is Element of Omega : k2 . w <= t } is Event of M ) by ASS, KJK;

then { w where w is Element of Omega : k1 . w <= t } /\ { w where w is Element of Omega : k2 . w <= t } is Event of M by PROB_1:19;

hence { w where w is Element of Omega : k2 . w <= t } /\ { w where w is Element of Omega : k1 . w <= t } in MyFunc . t ; :: thesis: verum

( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) ; :: thesis: verum