let X, Y be set ; :: thesis: ( [:X,Y:],[:(card X),Y:] are_equipotent & [:X,Y:],[:X,(card Y):] are_equipotent & [:X,Y:],[:(card X),(card Y):] are_equipotent & card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] )
( [:Y,X:],[:(card Y),X:] are_equipotent & [:X,Y:],[:Y,X:] are_equipotent ) by Lm2, Lm3;
then ( [:X,Y:],[:(card Y),X:] are_equipotent & [:(card Y),X:],[:X,(card Y):] are_equipotent ) by Lm2, WELLORD2:22;
hence A1: ( [:X,Y:],[:(card X),Y:] are_equipotent & [:X,Y:],[:X,(card Y):] are_equipotent ) by Lm3, WELLORD2:22; :: thesis: ( [:X,Y:],[:(card X),(card Y):] are_equipotent & card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] )
[:X,(card Y):],[:(card X),(card Y):] are_equipotent by Lm3;
hence [:X,Y:],[:(card X),(card Y):] are_equipotent by A1, WELLORD2:22; :: thesis: ( card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] )
hence ( card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] ) by A1, CARD_1:21; :: thesis: verum