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
then reconsider A = A9 as non empty finite set by CARD_1:27;
let a be Element of A9; :: thesis: ex b being Element of A9 st b <> a
{a} c= A by ZFMISC_1:31;
then card (A \ {a}) = (card A) - (card {a}) by CARD_2:44
.= (card A) - 1 by CARD_1:30 ;
then card (A \ {a}) <> 0 by A1;
then consider b being object such that
A2: b in A \ {a} by CARD_1:27, XBOOLE_0:def 1;
reconsider b = b as Element of A9 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