let X, Y be set ; :: thesis: ( (card X) +` (card Y) = card X & card Y in card X implies card (X \ Y) = card X )
assume A1: ( (card X) +` (card Y) = card X & card Y in card X ) ; :: thesis: card (X \ Y) = card X
X c= X \/ Y by XBOOLE_1:7;
then ( card X c= card (X \/ Y) & card (X \/ Y) c= card X ) by A1, CARD_1:27, CARD_2:47;
then A2: card (X \/ Y) = card X by XBOOLE_0:def 10;
( X \ Y misses Y & (X \ Y) \/ Y = X \/ Y ) by XBOOLE_1:39, XBOOLE_1:79;
then A3: card X = (card (X \ Y)) +` (card Y) by A2, CARD_2:48;
then A4: card (X \ Y) c= card X by Th72;

A5: now

assume not card X is finite ; :: thesis: card (X \ Y) = card X
then A6: (card X) +` (card X) = card X by Th33;
assume not card (X \ Y) = card X ; :: thesis: contradiction
then card (X \ Y) in card X by A4, CARD_1:13;
then card X in card X by A1, A3, A6, Th74;
hence contradiction ; :: thesis: verum

end;

now

assume card X is finite ; :: thesis: card (X \ Y) = card X
then reconsider X = X, Y = Y as finite set by A1, Th26;
( card X = card (card X) & card Y = card (card Y) ) ;
then card ((card X) + (card Y)) = card (card X) by A1, CARD_2:51;
then (card X) + (card Y) = (card X) + 0 by CARD_1:71;
then Y = {} ;
hence card (X \ Y) = card X ; :: thesis: verum

end;

hence card (X \ Y) = card X by A5; :: thesis: verum