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