let X be set ; :: thesis: for Si being SigmaField of X

for FSi being FinSequence of Si holds Intersection FSi in Si

let Si be SigmaField of X; :: thesis: for FSi being FinSequence of Si holds Intersection FSi in Si

let FSi be FinSequence of Si; :: thesis: Intersection FSi in Si

for FSi being FinSequence of Si holds Intersection FSi in Si

let Si be SigmaField of X; :: thesis: for FSi being FinSequence of Si holds Intersection FSi in Si

let FSi be FinSequence of Si; :: thesis: Intersection FSi in Si

per cases
( FSi = {} or FSi <> {} )
;

end;

suppose A1:
FSi <> {}
; :: thesis: Intersection FSi in Si

rng (Complement FSi) c= Si
;

then reconsider C = Complement FSi as FinSequence of Si by FINSEQ_1:def 4;

A2: Union C in Si by Th57;

Intersection FSi = (Union (Complement FSi)) ` by A1, Def6;

hence Intersection FSi in Si by A2, PROB_1:def 1; :: thesis: verum

end;then reconsider C = Complement FSi as FinSequence of Si by FINSEQ_1:def 4;

A2: Union C in Si by Th57;

Intersection FSi = (Union (Complement FSi)) ` by A1, Def6;

hence Intersection FSi in Si by A2, PROB_1:def 1; :: thesis: verum