let X1, X2, X3, X4 be set ; :: thesis: ( ( X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] ) implies X1 = {} )
assume that
A1: ( X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] ) and
A2: X1 <> {} ; :: thesis: contradiction
A3: ( [:X1,X2,X3,X4:] <> {} or [:X2,X3,X4,X1:] <> {} or [:X3,X4,X1,X2:] <> {} or [:X4,X1,X2,X3:] <> {} ) by A1, A2;
reconsider X1 = X1, X2 = X2, X3 = X3, X4 = X4 as non empty set by A3, Th39;

per cases ( X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] ) by A1;

suppose A4: X1 c= [:X1,X2,X3,X4:] ; :: thesis: contradiction

consider v being object such that
A5: v in X1 and
A6: for x1, x2, x3, x4 being object st ( x1 in X1 or x2 in X1 ) holds
v <> [x1,x2,x3,x4] by Th20;
reconsider v = v as Element of [:X1,X2,X3,X4:] by A4, A5;
v = [(v `1_4),(v `2_4),(v `3_4),(v `4_4)] ;
hence contradiction by A6; :: thesis: verum

end;

suppose X1 c= [:X2,X3,X4,X1:] ; :: thesis: contradiction

then X1 c= [:[:X2,X3:],X4,X1:] by Th38;
hence contradiction by Th34; :: thesis: verum

end;

suppose X1 c= [:X3,X4,X1,X2:] ; :: thesis: contradiction

then X1 c= [:[:X3,X4:],X1,X2:] by Th38;
hence contradiction by Th34; :: thesis: verum

end;

suppose A7: X1 c= [:X4,X1,X2,X3:] ; :: thesis: contradiction

consider v being object such that
A8: v in X1 and
A9: for x1, x2, x3, x4 being object st ( x1 in X1 or x2 in X1 ) holds
v <> [x1,x2,x3,x4] by Th20;
reconsider v = v as Element of [:X4,X1,X2,X3:] by A7, A8;
v = [(v `1_4),(v `2_4),(v `3_4),(v `4_4)] ;
hence contradiction by A9; :: thesis: verum

end;

end;