let A' be finite set ; :: thesis: ( card A' >= 3 implies for a, b being Element of A' ex c being Element of A' st
( c <> a & c <> b ) )
assume A1: card A' >= 3 ; :: thesis: for a, b being Element of A' ex c being Element of A' st
( c <> a & c <> b )
then reconsider A = A' as non empty finite set by CARD_1:47;
let a, b be Element of A'; :: thesis: ex c being Element of A' st
( c <> a & c <> b )
{a,b} c= A by ZFMISC_1:38;
then A2: 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, A2, XREAL_1:15;
then card (A \ {a,b}) <> 0 ;
then consider c being set such that
A3: c in A \ {a,b} by CARD_1:47, XBOOLE_0:def 1;
reconsider c = c as Element of A' 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