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;
then reconsider X = X, Y = Y, Z = Z as non empty set by Th21;
per cases ( X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] ) by A1;
suppose A3: X c= [:X,Y,Z:] ; :: thesis: contradiction
consider v being object such that
A4: v in X and
A5: for x, y, z being object st ( x in X or y in X ) holds
v <> [x,y,z] by Th19;
reconsider v = v as Element of [:X,Y,Z:] by A3, A4;
v = [(v `1_3),(v `2_3),(v `3_3)] ;
hence contradiction by A5; :: 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 ZFMISC_1:111; :: thesis: verum
end;
suppose A6: X c= [:Z,X,Y:] ; :: thesis: contradiction
consider v being object such that
A7: v in X and
A8: for z, x, y being object st ( z in X or x in X ) holds
v <> [z,x,y] by Th19;
reconsider v = v as Element of [:Z,X,Y:] by A6, A7;
v = [(v `1_3),(v `2_3),(v `3_3)] ;
hence contradiction by A8; :: thesis: verum
end;
end;