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]

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

end;