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 )
reconsider A = A9 as non empty finite set by A1, CARD_1:47;
let a, b be Element of A9; :: thesis: ex c being Element of A9 st
( c <> a & c <> b )
A2: {a,b} c= A by ZFMISC_1:38;
A3: card (A \ {a,b}) = (card A) - (card {a,b}) by A2, CARD_2:63;
A4: card {a,b} <= 2 by CARD_2:69;
A5: card (A \ {a,b}) >= 3 - 2 by A1, A3, A4, XREAL_1:15;
A6: card (A \ {a,b}) <> 0 by A5;
consider c being set such that
A7: c in A \ {a,b} by A6, CARD_1:47, XBOOLE_0:def 1;
reconsider c = c as Element of A9 by A7;
take c ; :: thesis: ( c <> a & c <> b )
A8: not c in {a,b} by A7, XBOOLE_0:def 5;
thus ( c <> a & c <> b ) by A8, TARSKI:def 2; :: thesis: verum