let x1, x2, x3, x4, x5, x6, x7 be set ; ( x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct implies card {x1,x2,x3,x4,x5,x6,x7} = 7 )
A1:
{x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7}
by ENUMSET1:21;
assume A2:
x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct
; card {x1,x2,x3,x4,x5,x6,x7} = 7
then A3:
x1 <> x3
by ZFMISC_1:def 9;
A4:
x5 <> x7
by A2, ZFMISC_1:def 9;
A5:
x4 <> x7
by A2, ZFMISC_1:def 9;
A6:
x3 <> x7
by A2, ZFMISC_1:def 9;
A7:
x2 <> x7
by A2, ZFMISC_1:def 9;
A8:
x4 <> x6
by A2, ZFMISC_1:def 9;
A9:
x4 <> x5
by A2, ZFMISC_1:def 9;
A10:
x5 <> x6
by A2, ZFMISC_1:def 9;
A11:
x1 <> x5
by A2, ZFMISC_1:def 9;
A12:
x1 <> x4
by A2, ZFMISC_1:def 9;
A13:
x3 <> x6
by A2, ZFMISC_1:def 9;
A14:
x3 <> x5
by A2, ZFMISC_1:def 9;
A15:
x3 <> x4
by A2, ZFMISC_1:def 9;
A16:
x2 <> x6
by A2, ZFMISC_1:def 9;
A17:
x2 <> x5
by A2, ZFMISC_1:def 9;
A18:
x2 <> x4
by A2, ZFMISC_1:def 9;
A19:
x2 <> x3
by A2, ZFMISC_1:def 9;
A20:
x1 <> x6
by A2, ZFMISC_1:def 9;
x1 <> x2
by A2, ZFMISC_1:def 9;
then
x1,x2,x3,x4,x5,x6 are_mutually_distinct
by A3, A12, A11, A20, A19, A18, A17, A16, A15, A14, A13, A9, A8, A10, ZFMISC_1:def 8;
then A21:
card {x1,x2,x3,x4,x5,x6} = 6
by Th2;
A22:
x6 <> x7
by A2, ZFMISC_1:def 9;
x1 <> x7
by A2, ZFMISC_1:def 9;
then
not x7 in {x1,x2,x3,x4,x5,x6}
by A7, A6, A5, A4, A22, ENUMSET1:def 4;
hence card {x1,x2,x3,x4,x5,x6,x7} =
6 + 1
by A21, A1, CARD_2:41
.=
7
;
verum