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 Th13, Th14;
then A2: X,[:(card X),{0 }:] are_equipotent by WELLORD2:22;
( Y,[:Y,{1}:] are_equipotent & [:Y,{1}:],[:(card Y),{1}:] are_equipotent ) by Th13, Th14;
then A3: Y,[:(card Y),{1}:] are_equipotent by WELLORD2:22;
[:(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:58;
hence card (X \/ Y) = card ([:(card X),{0 }:] \/ [:(card Y),{1}:]) by CARD_1:21
.= (card X) +` (card Y) by Th17 ;
:: thesis: verum