let x1, x2, x3, x4, x5, x6 be set ; :: thesis: ( 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} ; :: thesis: 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; :: thesis: verum