let X, Y be set ; :: thesis: ( X misses Y implies card (X \/ Y) = (card X) +` (card Y) )
assume A1: X misses Y ; :: thesis: card (X \/ Y) = (card X) +` (card Y)
( X,[:X,{0}:] are_equipotent & [:X,{0}:],[:(card X),{0}:] are_equipotent ) by CARD_1:69, Th6;
then A2: X,[:(card X),{0}:] are_equipotent by WELLORD2:15;
( Y,[:Y,{1}:] are_equipotent & [:Y,{1}:],[:(card Y),{1}:] are_equipotent ) by CARD_1:69, Th6;
then A3: Y,[:(card Y),{1}:] are_equipotent by WELLORD2:15;
[:(card X),{0}:] misses [:(card Y),{1}:] by Lm4;
then X \/ Y,[:(card X),{0}:] \/ [:(card Y),{1}:] are_equipotent by A1, A2, A3, CARD_1:31;
hence card (X \/ Y) = card ([:(card X),{0}:] \/ [:(card Y),{1}:]) by CARD_1:5
.= (card X) +` (card Y) by Th9 ;
:: thesis: verum