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 A1: [:X,Y:],[:(card Y),X:] are_equipotent by WELLORD2:22;
[:(card Y),X:],[:X,(card Y):] are_equipotent by Lm2;
hence A2: ( [:X,Y:],[:(card X),Y:] are_equipotent & [:X,Y:],[:X,(card Y):] are_equipotent ) by A1, 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 A2, 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 A2, CARD_1:21; :: thesis: verum