let X be set ; ( 3 c= card X iff ex x, y, z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )
thus
( 3 c= card X implies ex x, y, z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )
( ex x, y, z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z ) implies 3 c= card X )proof
assume
3
c= card X
;
ex x, y, z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
then
card 3
c= card X
;
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:10;
take x =
f . 0;
ex y, z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
take y =
f . 1;
ex z being object st
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
take z =
f . 2;
( x in X & y in X & z in X & x <> y & x <> z & y <> z )
A4:
0 in dom f
by A2, ENUMSET1:def 1, YELLOW11:1;
then
f . 0 in rng f
by FUNCT_1:def 3;
hence
x in X
by A3;
( y in X & z in X & x <> y & x <> z & y <> z )
A5:
1
in dom f
by A2, ENUMSET1:def 1, YELLOW11:1;
then
f . 1
in rng f
by FUNCT_1:def 3;
hence
y in X
by A3;
( z in X & x <> y & x <> z & y <> z )
A6:
2
in dom f
by A2, ENUMSET1:def 1, YELLOW11:1;
then
f . 2
in rng f
by FUNCT_1:def 3;
hence
z in X
by A3;
( x <> y & x <> z & y <> z )
thus
x <> y
by A1, A4, A5, FUNCT_1:def 4;
( x <> z & y <> z )
thus
x <> z
by A1, A4, A6, FUNCT_1:def 4;
y <> z
thus
y <> z
by A1, A5, A6, FUNCT_1:def 4;
verum
end;
given x, y, z being object such that A7:
( x in X & y in X & z in X )
and
A8:
( x <> y & x <> z & y <> z )
; 3 c= card X
{x,y,z} c= X
by A7, ENUMSET1:def 1;
then
card {x,y,z} c= card X
by CARD_1:11;
hence
3 c= card X
by A8, CARD_2:58; verum