let X, Y, Z be set ; :: thesis: ( ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) implies X = {} )
assume that
A1: ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) and
A2: X <> {} ; :: thesis: contradiction
( [:X,Y,Z:] <> {} or [:Y,Z,X:] <> {} or [:Z,X,Y:] <> {} ) by A1, A2, XBOOLE_1:3;
then A3: ( Y <> {} & Z <> {} ) by Th35;

per cases ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) by A1;

suppose A4: X c= [:X,Y,Z:] ; :: thesis: contradiction

consider v being set such that
A5: v in X and
A6: for x, y, z being set st ( x in X or y in X ) holds
v <> [x,y,z] by A2, Th29;
reconsider v = v as Element of [:X,Y,Z:] by A4, A5;
v = [(v `1),(v `2),(v `3)] by A2, A3, Th48;
hence contradiction by A2, A6; :: thesis: verum

end;

suppose X c= [:Y,Z,X:] ; :: thesis: contradiction

then X c= [:[:Y,Z:],X:] by ZFMISC_1:def 3;
hence contradiction by A2, ZFMISC_1:111; :: thesis: verum

end;

suppose A7: X c= [:Z,X,Y:] ; :: thesis: contradiction

consider v being set such that
A8: v in X and
A9: for z, x, y being set st ( z in X or x in X ) holds
v <> [z,x,y] by A2, Th29;
reconsider v = v as Element of [:Z,X,Y:] by A7, A8;
v = [(v `1),(v `2),(v `3)] by A2, A3, Th48;
hence contradiction by A2, A9; :: thesis: verum

end;

end;