let X1, X2, X3, X4, X5, X6, X7, X8 be set ; :: thesis: ( ( X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:] or X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:] or X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:] or X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:] or X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:] or X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:] or X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:] or X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:] ) implies X1 = {} )
assume that
A1: ( X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:] or X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:] or X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:] or X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:] or X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:] or X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:] or X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:] or X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:] ) and
A2: X1 <> {} ; :: thesis: contradiction
A3: ( [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} or [:X2,X3,X4,X5,X6,X7,X8,X1:] <> {} or [:X3,X4,X5,X6,X7,X8,X1,X2:] <> {} or [:X4,X5,X6,X7,X8,X1,X2,X3:] <> {} or [:X5,X6,X7,X8,X1,X2,X3,X4:] <> {} or [:X6,X7,X8,X1,X2,X3,X4,X5:] <> {} or [:X7,X8,X1,X2,X3,X4,X5,X6:] <> {} or [:X8,X1,X2,X3,X4,X5,X6,X7:] <> {} ) by A1, A2, XBOOLE_1:3;
then A4: ( X4 <> {} & X5 <> {} ) by Th132;
A5: X8 <> {} by A3, Th132;
A6: ( X6 <> {} & X7 <> {} ) by A3, Th132;
A7: ( X2 <> {} & X3 <> {} ) by A3, Th132;

now

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

suppose A8: X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:] ; :: thesis: contradiction

consider y being set such that
A9: y in X1 and
A10: for x1, x2, x3, x4, x5, x6, x7, x8 being set st ( x1 in X1 or x2 in X1 ) holds
y <> [x1,x2,x3,x4,x5,x6,x7,x8] by A2, Th125;
reconsider y = y as Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] by A8, A9;
y = [(y `1),(y `2),(y `3),(y `4),(y `5),(y `6),(y `7),(y `8)] by A2, A7, A4, A6, A5, Th138;
hence contradiction by A2, A10; :: thesis: verum

end;

suppose X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:] ; :: thesis: contradiction

then X1 c= [:[:X2,X3:],X4,X5,X6,X7,X8,X1:] by Th12;
hence contradiction by A2, Th98; :: thesis: verum

end;

suppose X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:] ; :: thesis: contradiction

then X1 c= [:[:X3,X4:],X5,X6,X7,X8,X1,X2:] by Th12;
hence contradiction by A2, Th98; :: thesis: verum

end;

suppose X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:] ; :: thesis: contradiction

then X1 c= [:[:X4,X5:],X6,X7,X8,X1,X2,X3:] by Th12;
hence contradiction by A2, Th98; :: thesis: verum

end;

suppose X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:] ; :: thesis: contradiction

then X1 c= [:[:X5,X6:],X7,X8,X1,X2,X3,X4:] by Th12;
hence contradiction by A2, Th98; :: thesis: verum

end;

suppose X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:] ; :: thesis: contradiction

then X1 c= [:[:X6,X7:],X8,X1,X2,X3,X4,X5:] by Th12;
hence contradiction by A2, Th98; :: thesis: verum

end;

suppose X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:] ; :: thesis: contradiction

then X1 c= [:[:X7,X8:],X1,X2,X3,X4,X5,X6:] by Th12;
hence contradiction by A2, Th98; :: thesis: verum

end;

suppose A11: X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:] ; :: thesis: contradiction

consider y being set such that
A12: y in X1 and
A13: for x1, x2, x3, x4, x5, x6, x7, x8 being set st ( x1 in X1 or x2 in X1 ) holds
y <> [x1,x2,x3,x4,x5,x6,x7,x8] by A2, Th125;
reconsider y = y as Element of [:X8,X1,X2,X3,X4,X5,X6,X7:] by A11, A12;
y = [(y `1),(y `2),(y `3),(y `4),(y `5),(y `6),(y `7),(y `8)] by A2, A7, A4, A6, A5, Th138;
hence contradiction by A2, A13; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum