let X, Y be finite set ; :: thesis: ( X c= Y & card X = card Y implies X = Y )
assume A1: ( X c= Y & card X = card Y ) ; :: thesis: X = Y
then card (Y \ X) = (card Y) - (card X) by CARD_2:63;
then Y \ X = {} by A1;
then Y c= X by XBOOLE_1:37;
hence X = Y by A1, XBOOLE_0:def 10; :: thesis: verum