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