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