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
A3: card (B \ A) = (card B) - (card A) by A1, CARD_2:63
.= 0 by A2 ;
A4: B \ A = {} by A3;
A5: B c= A by A4, XBOOLE_1:37;
thus A = B by A1, A5, XBOOLE_0:def 10; :: thesis: verum