set Ie = I \ ({} I);
sigUn (F,(I \ ({} I))) in futSigmaFields (F,I) by Def7;
hence not futSigmaFields (F,I) is empty ; :: thesis: verum