let X, Y be set ; :: thesis: ( (card X) +` (card Y) = card X & card Y in card X implies card (X \ Y) = card X )
assume that
A1: (card X) +` (card Y) = card X and
A2: card Y in card X ; :: thesis: card (X \ Y) = card X
A3: card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
card (X \/ Y) c= card X by A1, Th33;
then A4: card (X \/ Y) = card X by A3;
(X \ Y) \/ Y = X \/ Y by XBOOLE_1:39;
then A5: card X = (card (X \ Y)) +` (card Y) by A4, Th34, XBOOLE_1:79;
then A6: card (X \ Y) c= card X by Th93;
A7: now :: thesis: ( not card X is finite implies card (X \ Y) = card X )
assume not card X is finite ; :: thesis: card (X \ Y) = card X
then A8: (card X) +` (card X) = card X by Th74;
assume not card (X \ Y) = card X ; :: thesis: contradiction
then card (X \ Y) in card X by A6, CARD_1:3;
then card X in card X by A2, A5, A8, Th95;
hence contradiction ; :: thesis: verum
end;
now :: thesis: ( card X is finite implies card (X \ Y) = card X )
assume card X is finite ; :: thesis: card (X \ Y) = card X
then reconsider X = X, Y = Y as finite set by A2, CARD_3:92;
card Y = card (card Y) ;
then card ((card X) + (card Y)) = card (card X) by A1, Th37;
then (card X) + (card Y) = (card X) + 0 ;
then Y = {} ;
hence card (X \ Y) = card X ; :: thesis: verum
end;
hence card (X \ Y) = card X by A7; :: thesis: verum