defpred S₁[ set ] means (superior_setsequence A) . Omega is Event of Sigma;
(superior_setsequence A) . 0 = Union (A ^\ 0) by Def7;
then A1: S₁[ 0 ] by PROB_1:17;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume (superior_setsequence A) . k is Event of Sigma ; :: thesis: S₁[k + 1]
Union (A ^\ (k + 1)) in Sigma by PROB_1:17;
hence S₁[k + 1] by Def7; :: thesis: verum

end;

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