let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for k1, k2 being StoppingTime_Func of MyFunc st k1 <= k2 holds
Sigma_tau k1 c= Sigma_tau k2
let Sigma be SigmaField of Omega; :: thesis: for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for k1, k2 being StoppingTime_Func of MyFunc st k1 <= k2 holds
Sigma_tau k1 c= Sigma_tau k2
let r be Real; :: thesis: for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for k1, k2 being StoppingTime_Func of MyFunc st k1 <= k2 holds
Sigma_tau k1 c= Sigma_tau k2
let I be TheEvent of r; :: thesis: for MyFunc being Filtration of I,Sigma
for k1, k2 being StoppingTime_Func of MyFunc st k1 <= k2 holds
Sigma_tau k1 c= Sigma_tau k2
let MyFunc be Filtration of I,Sigma; :: thesis: for k1, k2 being StoppingTime_Func of MyFunc st k1 <= k2 holds
Sigma_tau k1 c= Sigma_tau k2
let k1, k2 be StoppingTime_Func of MyFunc; :: thesis: ( k1 <= k2 implies Sigma_tau k1 c= Sigma_tau k2 )
assume ASS0: k1 <= k2 ; :: thesis: Sigma_tau k1 c= Sigma_tau k2
set Jsigk1 = Sigma_tau k1;
set Jsigk2 = Sigma_tau k2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sigma_tau k1 or x in Sigma_tau k2 )
assume x in Sigma_tau k1 ; :: thesis: x in Sigma_tau k2
then consider A being Element of Sigma such that
Z1: ( x = A & ( for t being Element of I holds A /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } in MyFunc . t ) ) ;
reconsider x = x as Element of Sigma by Z1;
x in { A where A is Element of Sigma : for t being Element of I holds A /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } in MyFunc . t }

proof

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

proof

let t be Element of I; :: thesis: x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } in MyFunc . t
reconsider MyFt = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
set Imp0 = { w2 where w2 is Element of Omega : k2 . w2 <= t } ;
set Imp1 = x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ;
set Imp2 = (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ;
BU2: x /\ { w where w is Element of Omega : k1 . w <= t } is Event of MyFt by Z1;
L1: x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } c= (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } or y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } )
assume zw1: y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ; :: thesis: y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }
then ZW1: ( y in x & y in { w where w is Element of Omega : k2 . w <= t } ) by XBOOLE_0:def 4;
then consider w2 being Element of Omega such that
ZW2: ( y = w2 & k2 . w2 <= t ) ;
( k1 . w2 <= k2 . w2 & k2 . w2 <= t ) by ZW2, ASS0;
then k1 . w2 <= t by XXREAL_0:2;
then ( y in x & y in { w where w is Element of Omega : k1 . w <= t } ) by ZW2, zw1, XBOOLE_0:def 4;
then y in x /\ { w where w is Element of Omega : k1 . w <= t } by XBOOLE_0:def 4;
hence y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } by ZW1, XBOOLE_0:def 4; :: thesis: verum

end;

P1: x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } = (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }

proof

(x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } c= x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } or y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } )
assume y in (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ; :: thesis: y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t }
then ( y in x /\ { w where w is Element of Omega : k1 . w <= t } & y in { w2 where w2 is Element of Omega : k2 . w2 <= t } ) by XBOOLE_0:def 4;
then ( y in x & y in { w where w is Element of Omega : k1 . w <= t } & y in { w where w is Element of Omega : k2 . w <= t } ) by XBOOLE_0:def 4;
hence y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } by XBOOLE_0:def 4; :: thesis: verum

end;

hence x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } = (x /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } ) /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } by L1, TARSKI:2; :: thesis: verum

end;

x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } is Event of MyFt

proof

k2 is_StoppingTime_wrt MyFunc by Def1111;
then { w where w is Element of Omega : k2 . w <= t } is Event of MyFt ;
hence x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } is Event of MyFt by P1, BU2, PROB_1:19; :: thesis: verum

end;

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

end;

hence x in { A where A is Element of Sigma : for t being Element of I holds A /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } in MyFunc . t } ; :: thesis: verum

end;

hence x in Sigma_tau k2 ; :: thesis: verum