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