let A, B be finite set ; :: thesis: ( A c= B & card A = card B implies A = B )
assume that
A1: A c= B and
A2: card A = card B ; :: thesis: A = B
card (B \ A) = (card B) - (card A) by A1, CARD_2:63
.= 0 by A2 ;
then B \ A = {} ;
then B c= A by XBOOLE_1:37;
hence A = B by A1, XBOOLE_0:def 10; :: thesis: verum