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:47;
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:38;
then A3: card (A \ {a,b}) = (card A) - (card {a,b}) by CARD_2:63;
card {a,b} <= 2 by CARD_2:69;
then card (A \ {a,b}) >= 3 - 2 by A1, A3, XREAL_1:15;
then card (A \ {a,b}) <> 0 ;
then consider c being set such that
A7: c in A \ {a,b} by CARD_1:47, XBOOLE_0:def 1;
reconsider c = c as Element of A9 by A7;
take c ; :: thesis: ( c <> a & c <> b )
not c in {a,b} by A7, XBOOLE_0:def 5;
hence ( c <> a & c <> b ) by TARSKI:def 2; :: thesis: verum