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 and
A2: dom f = 3 and
A3: rng f c= X by CARD_1:26;
take x = f . 0 ; :: thesis:
take y = f . 1; :: thesis:
take z = f . 2; :: thesis:
A4: 0 in dom f by A2, ENUMSET1:def 1, YELLOW11:1;
then f . 0 in rng f by FUNCT_1:def 5;
hence x in X by A3; :: thesis:
A5: 1 in dom f by A2, ENUMSET1:def 1, YELLOW11:1;
then f . 1 in rng f by FUNCT_1:def 5;
hence y in X by A3; :: thesis:
A6: 2 in dom f by A2, ENUMSET1:def 1, YELLOW11:1;
then f . 2 in rng f by FUNCT_1:def 5;
hence z in X by A3; :: thesis:
thus x <> y by A1, A4, A5, FUNCT_1:def 8; :: thesis:
thus x <> z by A1, A4, A6, FUNCT_1:def 8; :: thesis:
thus y <> z by A1, A5, A6, FUNCT_1:def 8; :: thesis:

end;

given x, y, z being set such that A7: ( x in X & y in X & z in X ) and
A8: ( 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 A7, ENUMSET1:def 1; :: thesis:

end;

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