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

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