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 consider E being finite Subset of I such that
A0: X = sigUn F,(I \ E) by Def7;
thus {} in X by A0, PROB_1:10; :: thesis: verum

end;

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