for X being set st X in futSigmaFields F,I holds
{} in X

proof

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:10; :: thesis: verum

end;

hence not tailSigmaField F,I is empty by SETFAM_1:def 1; :: thesis: verum