for X being set st X in futSigmaFields (F,I) holds

{} in X

{} in X

proof

hence
not tailSigmaField (F,I) is empty
by SETFAM_1:def 1; :: thesis: verum
let X be set ; :: thesis: ( X in futSigmaFields (F,I) implies {} in X )

assume X in futSigmaFields (F,I) ; :: thesis: {} in X

then ex E being finite Subset of I st X = sigUn (F,(I \ E)) by Def7;

hence {} in X by PROB_1:4; :: thesis: verum

end;assume X in futSigmaFields (F,I) ; :: thesis: {} in X

then ex E being finite Subset of I st X = sigUn (F,(I \ E)) by Def7;

hence {} in X by PROB_1:4; :: thesis: verum