let x1, x2, x3, x4, x5, x6, x7 be set ; ( x1,x2,x3,x4,x5,x6 are_mutually_distinct & {x1,x2,x3,x4,x5,x6} misses {x7} implies x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct )
assume that
A1:
x1,x2,x3,x4,x5,x6 are_mutually_distinct
and
A2:
{x1,x2,x3,x4,x5,x6} misses {x7}
; x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct
A3:
x1 <> x3
by A1, ZFMISC_1:def 8;
A4:
x2 <> x3
by A1, ZFMISC_1:def 8;
A5:
x1 <> x6
by A1, ZFMISC_1:def 8;
A6:
x1 <> x5
by A1, ZFMISC_1:def 8;
A7:
x1 <> x4
by A1, ZFMISC_1:def 8;
A8:
not x7 in {x1,x2,x3,x4,x5,x6}
by A2, ZFMISC_1:48;
then A9:
x7 <> x1
by ENUMSET1:def 4;
A10:
x4 <> x6
by A1, ZFMISC_1:def 8;
A11:
x4 <> x5
by A1, ZFMISC_1:def 8;
A12:
x3 <> x6
by A1, ZFMISC_1:def 8;
A13:
x3 <> x5
by A1, ZFMISC_1:def 8;
A14:
x3 <> x4
by A1, ZFMISC_1:def 8;
A15:
x2 <> x6
by A1, ZFMISC_1:def 8;
A16:
x2 <> x5
by A1, ZFMISC_1:def 8;
A17:
x2 <> x4
by A1, ZFMISC_1:def 8;
A18:
x7 <> x6
by A8, ENUMSET1:def 4;
A19:
x5 <> x6
by A1, ZFMISC_1:def 8;
A20:
x7 <> x5
by A8, ENUMSET1:def 4;
A21:
x7 <> x4
by A8, ENUMSET1:def 4;
A22:
x7 <> x3
by A8, ENUMSET1:def 4;
A23:
x7 <> x2
by A8, ENUMSET1:def 4;
x1 <> x2
by A1, ZFMISC_1:def 8;
hence
x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct
by A3, A7, A6, A5, A4, A17, A16, A15, A14, A13, A12, A11, A10, A19, A9, A23, A22, A21, A20, A18, ZFMISC_1:def 9; verum