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