let X, Y be set ; :: thesis: ( not X is finite & ( X,Y are_equipotent or Y,X are_equipotent ) implies ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) )
assume ( not X is finite & ( X,Y are_equipotent or Y,X are_equipotent ) ) ; :: thesis: ( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
then ( not card X is finite & card X = card Y & X c= X \/ Y ) by CARD_1:21, XBOOLE_1:7;
then ( card X c= card (X \/ Y) & card (X \/ Y) c= (card X) +` (card Y) & (card X) +` (card Y) = card X ) by Th33, CARD_1:27, CARD_2:47;
then card X = card (X \/ Y) by XBOOLE_0:def 10;
hence ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) by CARD_1:21; :: thesis: verum