theorem Th1: :: CARDFIL4:1

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