let X1, X2 be finite set ; :: thesis: ( X1 c= X2 & card X1 = card X2 implies X1 = X2 )
assume AS: ( X1 c= X2 & card X1 = card X2 ) ; :: thesis: X1 = X2
then card (X2 \ X1) = (card X2) - (card X1) by CARD_2:44
.= 0 by AS ;
then X2 \ X1 = {} ;
then X2 c= X1 by XBOOLE_1:37;
hence X1 = X2 by AS, XBOOLE_0:def 10; :: thesis: verum