let X be set ; :: thesis:
thus ( 3 c= card X implies ex x, y, z being set st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) ) :: thesis:

assume 3 c= card X ; :: thesis:
then card 3 c= card X by CARD_1:def 5;
then consider f being Function such that
A1: ( f is one-to-one & dom f = 3 & rng f c= X ) by CARD_1:26;
take x = f . 0 ; :: thesis:
take y = f . 1; :: thesis:
take z = f . 2; :: thesis:
A2: ( 0 in dom f & 1 in dom f & 2 in dom f ) by A1, ENUMSET1:def 1, YELLOW11:1;
then f . 0 in rng f by FUNCT_1:def 5;
hence x in X by A1; :: thesis:
f . 1 in rng f by A2, FUNCT_1:def 5;
hence y in X by A1; :: thesis:
f . 2 in rng f by A2, FUNCT_1:def 5;
hence z in X by A1; :: thesis:
thus x <> y by A1, A2, FUNCT_1:def 8; :: thesis:
thus x <> z by A1, A2, FUNCT_1:def 8; :: thesis:
thus y <> z by A1, A2, FUNCT_1:def 8; :: thesis:

end;

given x, y, z being set such that A3: ( x in X & y in X & z in X & x <> y & x <> z & y <> z ) ; :: thesis:
{x,y,z} c= X

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {x,y,z} ; :: thesis:
hence a in X by A3, ENUMSET1:def 1; :: thesis:

end;

then card {x,y,z} c= card X by CARD_1:27;
hence 3 c= card X by A3, CARD_2:77; :: thesis: