let x1, x2, x3, x4, x5, x6, x7 be set ; ( x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct implies x7,x1,x2,x3,x4,x5,x6 are_mutually_distinct )
assume A1:
x1,x2,x3,x4,x5,x6,x7 are_mutually_distinct
; x7,x1,x2,x3,x4,x5,x6 are_mutually_distinct
then A2:
x1 <> x3
by ZFMISC_1:def 9;
A3:
x5 <> x7
by A1, ZFMISC_1:def 9;
A4:
x5 <> x6
by A1, ZFMISC_1:def 9;
A5:
x4 <> x7
by A1, ZFMISC_1:def 9;
A6:
x4 <> x6
by A1, ZFMISC_1:def 9;
A7:
x6 <> x7
by A1, ZFMISC_1:def 9;
A8:
x1 <> x5
by A1, ZFMISC_1:def 9;
A9:
x1 <> x4
by A1, ZFMISC_1:def 9;
A10:
x2 <> x4
by A1, ZFMISC_1:def 9;
A11:
x2 <> x3
by A1, ZFMISC_1:def 9;
A12:
x1 <> x7
by A1, ZFMISC_1:def 9;
A13:
x1 <> x6
by A1, ZFMISC_1:def 9;
A14:
x4 <> x5
by A1, ZFMISC_1:def 9;
A15:
x3 <> x7
by A1, ZFMISC_1:def 9;
A16:
x3 <> x6
by A1, ZFMISC_1:def 9;
A17:
x3 <> x5
by A1, ZFMISC_1:def 9;
A18:
x3 <> x4
by A1, ZFMISC_1:def 9;
A19:
x2 <> x7
by A1, ZFMISC_1:def 9;
A20:
x2 <> x6
by A1, ZFMISC_1:def 9;
A21:
x2 <> x5
by A1, ZFMISC_1:def 9;
x1 <> x2
by A1, ZFMISC_1:def 9;
hence
x7,x1,x2,x3,x4,x5,x6 are_mutually_distinct
by A2, A9, A8, A13, A12, A11, A10, A21, A20, A19, A18, A17, A16, A15, A14, A6, A5, A4, A3, A7, ZFMISC_1:def 9; verum