let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let r be Real; :: thesis:
let I be TheEvent of r; :: thesis:
let MyFunc be Filtration of I,Sigma; :: thesis:
let k1, k2 be StoppingTime_Func of MyFunc; :: thesis:
assume ASS0: k1 <= k2 ; :: thesis:
set Jsigk1 = Sigma_tau k1;
set Jsigk2 = Sigma_tau k2;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Sigma_tau k1 ; :: thesis:
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 }

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

let t be Element of I; :: thesis:
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:
assume zw1: y in x /\ { w2 where w2 is Element of Omega : k2 . w2 <= t } ; :: thesis:
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:

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

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:

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:

end;

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

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:

end;

hence x in Sigma_tau k2 ; :: thesis: