let x1, x2, x3, x4, x5, x6 be set ; ( {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}
; ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 )
A2:
x5 in {x4,x5,x6}
by ENUMSET1:def 1;
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 )
; contradiction
then A3:
( x4 in {x1,x2,x3} or x5 in {x1,x2,x3} or x6 in {x1,x2,x3} )
by ENUMSET1:def 1;
A4:
x6 in {x4,x5,x6}
by ENUMSET1:def 1;
x4 in {x4,x5,x6}
by ENUMSET1:def 1;
hence
contradiction
by A1, A3, A2, A4, XBOOLE_0:3; verum