now

let n be Nat; :: thesis: (Complement S) . n in Si
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
X: S . n in rng S by NAT_1:52;
rng S c= Si by RELAT_1:def 19;
then S . n in Si by X;
then A0: S . n is Event of Si ;
(Complement S) . n = (S . n1) ` by PROB_1:def 4;
then (Complement S) . n is Event of Si by A0, PROB_1:50;
hence (Complement S) . n in Si ; :: thesis: verum

end;

then rng (Complement S) c= Si by NAT_1:53;
hence Complement S is SetSequence of by RELAT_1:def 19; :: thesis: verum