let X, Y be set ; :: thesis: ( X is infinite & Y is finite implies X \ Y is infinite )
X \/ Y = (X \ Y) \/ Y by XBOOLE_1:39;
hence ( X is infinite & Y is finite implies X \ Y is infinite ) by Th3; :: thesis: verum