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)

proof

rng (max (k1,k2)) c= StoppingSetExt T

proof

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

proof

per cases ( k2 . x2 <= k1 . x2 or not k2 . x2 <= k1 . x2 ) ;

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;

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;

end;

end;

hence x in StoppingSetExt T by Def20, C1; :: thesis: verum

end;

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

end;

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

proof

for t being Element of StoppingSet T holds { w where w is Element of Omega : k3 . w <= t } in MyFunc . t

proof

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 ) }

proof

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 ) } )

proof

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 } )

proof

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;

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

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;

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;

end;

end;

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 }
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;

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

end;

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 }

proof

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 } )

proof

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 ) } )

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 : 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;

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 ) }
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;

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

end;

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

proof

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;

hence { w where w is Element of Omega : k3 . w <= t } in MyFunc . t by O2, O1; :: thesis: verum

end;

hence k3 is_StoppingTime_wrt MyFunc,T by KJK; :: thesis: verum

end;

hence ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T ) ; :: thesis: verum