let A' be finite set ; :: thesis: ( card A' >= 2 implies for a being Element of A' ex b being Element of A' st b <> a )
assume A1: card A' >= 2 ; :: thesis: for a being Element of A' ex b being Element of A' st b <> a
then reconsider A = A' as non empty finite set by CARD_1:47;
let a be Element of A'; :: thesis: ex b being Element of A' st b <> a
{a} c= A by ZFMISC_1:37;
then card (A \ {a}) = (card A) - (card {a}) by CARD_2:63
.= (card A) - 1 by CARD_1:50 ;
then card (A \ {a}) <> 0 by A1;
then consider b being set such that
A2: b in A \ {a} by CARD_1:47, XBOOLE_0:def 1;
reconsider b = b as Element of A' by A2;
take b ; :: thesis: b <> a
not b in {a} by A2, XBOOLE_0:def 5;
hence b <> a by TARSKI:def 1; :: thesis: verum