let X, Y be set ; ( 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 that
A1:
not X is finite
and
A2:
( X,Y are_equipotent or Y,X are_equipotent )
; ( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
A3:
card X = card Y
by A2, CARD_1:5;
A4:
card X c= card (X \/ Y)
by CARD_1:11, XBOOLE_1:7;
A5:
card (X \/ Y) c= (card X) +` (card Y)
by Th33;
(card X) +` (card Y) = card X
by A1, A3, Th74;
then
card X = card (X \/ Y)
by A4, A5;
hence
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
by CARD_1:5; verum