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

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