let X, Z be set ; :: thesis: for W being finite Subset of X st X \ W c= Z holds
X \ Z is finite
let W be finite Subset of X; :: thesis: ( X \ W c= Z implies X \ Z is finite )
assume X \ W c= Z ; :: thesis: X \ Z is finite
then X \ Z c= X \ (X \ W) by XBOOLE_1:34;
then X \ Z c= X /\ W by XBOOLE_1:48;
hence X \ Z is finite ; :: thesis: verum