theorem Th2: :: CARDFIL4:2

for X, Z being set st Z c= X & X \ Z is finite holds
ex W being finite Subset of X st X \ W = Z