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:4; :: thesis: verum
end;
hence not tailSigmaField (F,I) is empty by SETFAM_1:def 1; :: thesis: verum