let X1, X2, X3 be set ; ( not X1 in X2 or not X2 in X3 or not X3 in X1 )
A1:
( X2 in {X1,X2,X3} & X3 in {X1,X2,X3} )
by ENUMSET1:def 1;
A2:
X1 in {X1,X2,X3}
by ENUMSET1:def 1;
then consider T being set such that
A3:
T in {X1,X2,X3}
and
A4:
{X1,X2,X3} misses T
by Th1;
( T = X1 or T = X2 or T = X3 )
by A3, ENUMSET1:def 1;
hence
( not X1 in X2 or not X2 in X3 or not X3 in X1 )
by A2, A1, A4, XBOOLE_0:3; verum