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

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