let A, B be finite set ; :: thesis: ( A c= B & card A = card B implies A = B )
assume A1: A c= B ; :: thesis: ( not card A = card B or A = B )
assume A2: card A = card B ; :: thesis: A = B
reconsider A = A as Subset of B by A1;
set f = incl A;
rng (incl A) = B by A2, FINSEQ_4:78;
hence A = B by RELAT_1:71; :: thesis: verum