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 & Y,[:Y,{1}:] are_equipotent & [:Y,{1}:],[:(card Y),{1}:] are_equipotent ) by Th13, Th14;
then ( [:(card X),{0 }:] misses [:(card Y),{1}:] & X,[:(card X),{0 }:] are_equipotent & Y,[:(card Y),{1}:] are_equipotent ) by Lm4, WELLORD2:22;
then X \/ Y,[:(card X),{0 }:] \/ [:(card Y),{1}:] are_equipotent by A1, 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