let x1, x2, x3, x4, x5, x6 be set ; ( x1,x2,x3 are_mutually_distinct & x4,x5,x6 are_mutually_distinct & {x1,x2,x3} misses {x4,x5,x6} implies x1,x2,x3,x4,x5,x6 are_mutually_distinct )
assume that
A1:
x1,x2,x3 are_mutually_distinct
and
A2:
x4,x5,x6 are_mutually_distinct
and
A3:
{x1,x2,x3} misses {x4,x5,x6}
; x1,x2,x3,x4,x5,x6 are_mutually_distinct
A4:
x1 <> x2
by A1, ZFMISC_1:def 5;
A5:
x3 <> x5
by A3, Th4;
A6:
x3 <> x4
by A3, Th4;
A7:
x1 <> x6
by A3, Th4;
A8:
x1 <> x3
by A1, ZFMISC_1:def 5;
A9:
x2 <> x5
by A3, Th4;
A10:
x5 <> x6
by A2, ZFMISC_1:def 5;
A11:
x2 <> x4
by A3, Th4;
A12:
x4 <> x5
by A2, ZFMISC_1:def 5;
A13:
x2 <> x6
by A3, Th4;
A14:
x4 <> x6
by A2, ZFMISC_1:def 5;
A15:
x3 <> x6
by A3, Th4;
A16:
x1 <> x5
by A3, Th4;
A17:
x2 <> x3
by A1, ZFMISC_1:def 5;
x1 <> x4
by A3, Th4;
hence
x1,x2,x3,x4,x5,x6 are_mutually_distinct
by A4, A17, A8, A12, A10, A14, A16, A7, A11, A9, A13, A6, A5, A15, ZFMISC_1:def 8; verum