defpred S₁[ set ] means (inferior_setsequence A) . Omega is Event of Sigma;
A1: Union (Complement (A ^\ 0)) is Event of Sigma by PROB_1:26;
(inferior_setsequence A) . 0 = Intersection (A ^\ 0) by Def9;
then A2: S₁[ 0 ] by A1, PROB_1:20;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume (inferior_setsequence A) . k is Event of Sigma ; :: thesis: S₁[k + 1]
A4: Union (Complement (A ^\ (k + 1))) is Event of Sigma by PROB_1:26;
(inferior_setsequence A) . (k + 1) = Intersection (A ^\ (k + 1)) by Def9;
hence S₁[k + 1] by A4, PROB_1:20; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence inferior_setsequence A is Sigma -valued by PROB_1:25; :: thesis: verum