let X1, X2, X3, X4 be set ; :: thesis: ( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X1 )
A1: ( X1 in {X1,X2,X3,X4} & X2 in {X1,X2,X3,X4} & X3 in {X1,X2,X3,X4} & X4 in {X1,X2,X3,X4} ) by ENUMSET1:def 2;
then consider T being set such that
A2: T in {X1,X2,X3,X4} and
A3: for x being set holds
( not x in {X1,X2,X3,X4} or not x in T ) by TARSKI:7;
( T = X1 or T = X2 or T = X3 or T = X4 ) by A2, ENUMSET1:def 2;
hence ( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X1 ) by A1, A3; :: thesis: verum