let X, Y, Z be set ; :: thesis: ( not X in Y or not Y in Z or not Z in X )
A1: ( Y in {X,Y,Z} & Z in {X,Y,Z} ) by ENUMSET1:def 1;
A2: X in {X,Y,Z} by ENUMSET1:def 1;
then consider T being set such that
A3: T in {X,Y,Z} and
A4: for x being set holds
( not x in {X,Y,Z} or not x in T ) by TARSKI:2;
( T = X or T = Y or T = Z ) by A3, ENUMSET1:def 1;
hence ( not X in Y or not Y in Z or not Z in X ) by A2, A1, A4; :: thesis: verum