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

assume 4 c= card X ; :: thesis:
then card 4 c= card X ;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = 4 and
A3: rng f c= X by CARD_1:10;
take w = f . 0; :: thesis:
take x = f . 1; :: thesis:
take y = f . 2; :: thesis:
take z = f . 3; :: thesis:
A4: 0 in dom f by A2, ENUMSET1:def 2, CARD_1:52;
then f . 0 in rng f by FUNCT_1:def 3;
hence w in X by A3; :: thesis:
A5: 1 in dom f by A2, ENUMSET1:def 2, CARD_1:52;
then f . 1 in rng f by FUNCT_1:def 3;
hence x in X by A3; :: thesis:
A6: 2 in dom f by A2, ENUMSET1:def 2, CARD_1:52;
then f . 2 in rng f by FUNCT_1:def 3;
hence y in X by A3; :: thesis:
A7: 3 in dom f by A2, ENUMSET1:def 2, CARD_1:52;
then f . 3 in rng f by FUNCT_1:def 3;
hence z in X by A3; :: thesis:
thus w <> x by A1, A4, A5, FUNCT_1:def 4; :: thesis:
thus w <> y by A1, A4, A6, FUNCT_1:def 4; :: thesis:
thus w <> z by A1, A4, A7, FUNCT_1:def 4; :: thesis:
thus x <> y by A1, A5, A6, FUNCT_1:def 4; :: thesis:
thus x <> z by A1, A5, A7, FUNCT_1:def 4; :: thesis:
thus y <> z by A1, A6, A7, FUNCT_1:def 4; :: thesis:

end;

given w, x, y, z being object such that A8: ( w in X & x in X & y in X & z in X ) and
A9: ( w <> x & w <> y & w <> z & x <> y & x <> z & y <> z ) ; :: thesis:
for a being object st a in {w,x,y,z} holds
a in X by A8, ENUMSET1:def 2;
then card {w,x,y,z} c= card X by TARSKI:def 3, CARD_1:11;
hence 4 c= card X by A9, CARD_2:59; :: thesis: