let X, Z be set ; :: thesis: ( Z c= X & X \ Z is finite implies ex W being finite Subset of X st X \ W = Z )
assume that
A1: Z c= X and
A2: X \ Z is finite ; :: thesis: ex W being finite Subset of X st X \ W = Z
X \ (X \ Z) = X /\ Z by XBOOLE_1:48
.= Z by A1, XBOOLE_1:17, XBOOLE_1:19 ;
hence ex W being finite Subset of X st X \ W = Z by A2; :: thesis: verum