defpred S_{1}[ set ] means (Intersect_Shift_Seq A) . Omega is Event of Sigma;

A1: Union (Complement (A ^\ 0)) is Event of Sigma by PROB_1:26;

(Intersect_Shift_Seq A) . 0 = Intersection (A ^\ 0) by Def9;

then A2: S_{1}[ 0 ]
by A1, PROB_1:20;

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A2, A3);

hence Intersect_Shift_Seq A is Sigma -valued by PROB_1:25; :: thesis: verum

A1: Union (Complement (A ^\ 0)) is Event of Sigma by PROB_1:26;

(Intersect_Shift_Seq A) . 0 = Intersection (A ^\ 0) by Def9;

then A2: S

A3: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume (Intersect_Shift_Seq A) . k is Event of Sigma ; :: thesis: S_{1}[k + 1]

A4: Union (Complement (A ^\ (k + 1))) is Event of Sigma by PROB_1:26;

(Intersect_Shift_Seq A) . (k + 1) = Intersection (A ^\ (k + 1)) by Def9;

hence S_{1}[k + 1]
by A4, PROB_1:20; :: thesis: verum

end;assume (Intersect_Shift_Seq A) . k is Event of Sigma ; :: thesis: S

A4: Union (Complement (A ^\ (k + 1))) is Event of Sigma by PROB_1:26;

(Intersect_Shift_Seq A) . (k + 1) = Intersection (A ^\ (k + 1)) by Def9;

hence S

hence Intersect_Shift_Seq A is Sigma -valued by PROB_1:25; :: thesis: verum