set MySigmatau = { A where A is Element of Sigma : for t2 being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 } ;
A1 . n in rng A1 by FUNCT_2:4, ORDINAL1:def 12;
then A1 . n in { A where A is Element of Sigma : for t2 being Element of S holds A /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 } by LOC1;
then consider B being Element of Sigma such that
GW1: ( A1 . n = B & ( for t2 being Element of S holds B /\ { w where w is Element of Omega : tau . w <= t2 } in MyFunc . t2 ) ) ;
reconsider A1n = A1 . n as Element of Sigma by GW1;
GW2: for t being Element of S holds ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
proof
let t be Element of S; :: thesis: ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t
reconsider MyFt2 = MyFunc . t as SigmaField of Omega by KOLMOG01:def 2;
set F = { w where w is Element of Omega : tau . w <= t } ;
J1: { w where w is Element of Omega : tau . w <= t } c= Omega
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { w where w is Element of Omega : tau . w <= t } or b in Omega )
assume b in { w where w is Element of Omega : tau . w <= t } ; :: thesis: b in Omega
then consider ww being Element of Omega such that
L1: ( ww = b & tau . ww <= t ) ;
thus b in Omega by L1; :: thesis: verum
end;
E1: { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) = { w where w is Element of Omega : tau . w <= t } \ (A1 . n) by XBOOLE_1:47
.= { w where w is Element of Omega : tau . w <= t } /\ ((A1 . n) `) by J1, SUBSET_1:13 ;
W2: (A1 . n) /\ { w where w is Element of Omega : tau . w <= t } is Event of MyFt2 by GW1;
tau is_StoppingTime_wrt MyFunc,S by Def11111;
then { w where w is Element of Omega : tau . w <= t } is Event of MyFt2 ;
then { w where w is Element of Omega : tau . w <= t } \ ((A1 . n) /\ { w where w is Element of Omega : tau . w <= t } ) is Event of MyFt2 by W2, PROB_1:24;
hence ((A1 . n) `) /\ { w where w is Element of Omega : tau . w <= t } in MyFunc . t by E1; :: thesis: verum
end;
(A1 . n) ` = (Complement A1) . n by PROB_1:def 2;
hence ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc) by GW2; :: thesis: verum