let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for S being non empty Subset of REAL

for MyFunc being Filtration of S,Sigma

for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let Sigma be SigmaField of Omega; :: thesis: for S being non empty Subset of REAL

for MyFunc being Filtration of S,Sigma

for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let S be non empty Subset of REAL; :: thesis: for MyFunc being Filtration of S,Sigma

for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let MyFunc be Filtration of S,Sigma; :: thesis: for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let k1, k2 be StoppingTime_Func of Sigma,MyFunc; :: thesis: ( k1 <= k2 implies Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2) )

assume ASS0: k1 <= k2 ; :: thesis: Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sigma_tau (MyFunc,k1) or x in Sigma_tau (MyFunc,k2) )

assume x in Sigma_tau (MyFunc,k1) ; :: thesis: x in Sigma_tau (MyFunc,k2)

then consider A being Element of Sigma such that

Z1: ( x = A & ( for t being Element of S holds A /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } in MyFunc . t ) ) ;

reconsider x = x as Element of Sigma by Z1;

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

for S being non empty Subset of REAL

for MyFunc being Filtration of S,Sigma

for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let Sigma be SigmaField of Omega; :: thesis: for S being non empty Subset of REAL

for MyFunc being Filtration of S,Sigma

for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let S be non empty Subset of REAL; :: thesis: for MyFunc being Filtration of S,Sigma

for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let MyFunc be Filtration of S,Sigma; :: thesis: for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds

Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let k1, k2 be StoppingTime_Func of Sigma,MyFunc; :: thesis: ( k1 <= k2 implies Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2) )

assume ASS0: k1 <= k2 ; :: thesis: Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sigma_tau (MyFunc,k1) or x in Sigma_tau (MyFunc,k2) )

assume x in Sigma_tau (MyFunc,k1) ; :: thesis: x in Sigma_tau (MyFunc,k2)

then consider A being Element of Sigma such that

Z1: ( x = A & ( for t being Element of S holds A /\ { w2 where w2 is Element of Omega : k1 . w2 <= t } in MyFunc . t ) ) ;

reconsider x = x as Element of Sigma by Z1;

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

proof

hence
x in Sigma_tau (MyFunc,k2)
; :: thesis: verum
let t be Element of S; :: 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;

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 }

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

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 : k2 . w2 <= t } is Event of MyFt
thus
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 }
:: according to XBOOLE_0:def 10 :: thesis: (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 }

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

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

proof

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

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