let x1, x2, x3, x4, x5, x6 be set ; :: thesis: ( {x1,x2,x3} misses {x4,x5,x6} implies ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 ) )
assume A1: {x1,x2,x3} misses {x4,x5,x6} ; :: thesis: ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 )
assume ( x1 = x4 or x1 = x5 or x1 = x6 or x2 = x4 or x2 = x5 or x2 = x6 or x3 = x4 or x3 = x5 or x3 = x6 ) ; :: thesis: contradiction
then A2: ( x4 in {x1,x2,x3} or x5 in {x1,x2,x3} or x6 in {x1,x2,x3} ) by ENUMSET1:def 1;
( x4 in {x4,x5,x6} & x5 in {x4,x5,x6} & x6 in {x4,x5,x6} ) by ENUMSET1:def 1;
hence contradiction by A1, A2, XBOOLE_0:3; :: thesis: verum