assume not COMPLEMENT F is empty ; :: thesis: contradiction
then ex x being Subset of X st x in COMPLEMENT F by SUBSET_1:4;
hence contradiction by Def7; :: thesis: verum