let A9 be finite set ; :: thesis: ( card A9 >= 3 implies for a, b being Element of A9 ex c being Element of A9 st

( c <> a & c <> b ) )

assume A1: card A9 >= 3 ; :: thesis: for a, b being Element of A9 ex c being Element of A9 st

( c <> a & c <> b )

then reconsider A = A9 as non empty finite set by CARD_1:27;

let a, b be Element of A9; :: thesis: ex c being Element of A9 st

( c <> a & c <> b )

{a,b} c= A by ZFMISC_1:32;

then A2: card (A \ {a,b}) = (card A) - (card {a,b}) by CARD_2:44;

card {a,b} <= 2 by CARD_2:50;

then card (A \ {a,b}) >= 3 - 2 by A1, A2, XREAL_1:13;

then card (A \ {a,b}) <> 0 ;

then consider c being object such that

A3: c in A \ {a,b} by CARD_1:27, XBOOLE_0:def 1;

reconsider c = c as Element of A9 by A3;

take c ; :: thesis: ( c <> a & c <> b )

not c in {a,b} by A3, XBOOLE_0:def 5;

hence ( c <> a & c <> b ) by TARSKI:def 2; :: thesis: verum

( c <> a & c <> b ) )

assume A1: card A9 >= 3 ; :: thesis: for a, b being Element of A9 ex c being Element of A9 st

( c <> a & c <> b )

then reconsider A = A9 as non empty finite set by CARD_1:27;

let a, b be Element of A9; :: thesis: ex c being Element of A9 st

( c <> a & c <> b )

{a,b} c= A by ZFMISC_1:32;

then A2: card (A \ {a,b}) = (card A) - (card {a,b}) by CARD_2:44;

card {a,b} <= 2 by CARD_2:50;

then card (A \ {a,b}) >= 3 - 2 by A1, A2, XREAL_1:13;

then card (A \ {a,b}) <> 0 ;

then consider c being object such that

A3: c in A \ {a,b} by CARD_1:27, XBOOLE_0:def 1;

reconsider c = c as Element of A9 by A3;

take c ; :: thesis: ( c <> a & c <> b )

not c in {a,b} by A3, XBOOLE_0:def 5;

hence ( c <> a & c <> b ) by TARSKI:def 2; :: thesis: verum