let X, Y be finite set ; :: thesis: ( X c= Y & card X = card Y implies X = Y )
assume that
A1: X c= Y and
A2: card X = card Y ; :: thesis: X = Y
card (Y \ X) = (card Y) - (card X) by A1, Th43;
then Y \ X = {} by A2;
then Y c= X by XBOOLE_1:37;
hence X = Y by A1; :: thesis: verum