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
per cases ( FSi = {} or FSi <> {} ) ;
suppose FSi = {} ; :: thesis: Intersection FSi in Si
then Intersection FSi = {} by Def6;
hence Intersection FSi in Si by PROB_1:4; :: thesis: verum
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;
end;