let X be infinite set ; :: thesis: X in { (X \ A) where A is finite Subset of X : verum }
set Z = {} ;
{} is finite Subset of X
proof
{} c= X ;
hence {} is finite Subset of X ; :: thesis: verum
end;
then reconsider Z = {} as finite Subset of X ;
X \ Z in { (X \ A) where A is finite Subset of X : verum } ;
hence X in { (X \ A) where A is finite Subset of X : verum } ; :: thesis: verum