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