theorem :: FINSET_1:4

for A, B being set st A is finite holds
A \ B is finite ;