let x1, x2, x3, x4, x5, x6 be set ; ( x1,x2,x3,x4,x5,x6 are_mutually_distinct implies card {x1,x2,x3,x4,x5,x6} = 6 )
A1:
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6}
by ENUMSET1:15;
assume A2:
x1,x2,x3,x4,x5,x6 are_mutually_distinct
; card {x1,x2,x3,x4,x5,x6} = 6
then A3:
x1 <> x3
by ZFMISC_1:def 8;
A4:
x4 <> x5
by A2, ZFMISC_1:def 8;
A5:
x3 <> x5
by A2, ZFMISC_1:def 8;
A6:
x3 <> x4
by A2, ZFMISC_1:def 8;
A7:
x2 <> x5
by A2, ZFMISC_1:def 8;
A8:
x2 <> x4
by A2, ZFMISC_1:def 8;
A9:
x2 <> x3
by A2, ZFMISC_1:def 8;
A10:
x1 <> x5
by A2, ZFMISC_1:def 8;
A11:
x1 <> x4
by A2, ZFMISC_1:def 8;
x1 <> x2
by A2, ZFMISC_1:def 8;
then
x1,x2,x3,x4,x5 are_mutually_distinct
by A3, A11, A10, A9, A8, A7, A6, A5, A4, ZFMISC_1:def 7;
then A12:
card {x1,x2,x3,x4,x5} = 5
by CARD_2:63;
A13:
x3 <> x6
by A2, ZFMISC_1:def 8;
A14:
x2 <> x6
by A2, ZFMISC_1:def 8;
A15:
x5 <> x6
by A2, ZFMISC_1:def 8;
A16:
x4 <> x6
by A2, ZFMISC_1:def 8;
x1 <> x6
by A2, ZFMISC_1:def 8;
then
not x6 in {x1,x2,x3,x4,x5}
by A14, A13, A16, A15, ENUMSET1:def 3;
hence card {x1,x2,x3,x4,x5,x6} =
5 + 1
by A12, A1, CARD_2:41
.=
6
;
verum