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

now

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

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

consider x being set such that
A5: x in X1 and
A6: for x1, x2, x3, x4, x5 being set st ( x1 in X1 or x2 in X1 ) holds
x <> [x1,x2,x3,x4,x5] by A2, Th8;
reconsider x = x as Element of [:X1,X2,X3,X4,X5:] by A4, A5;
( x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )] & x `1 in X1 ) by A3, Th19;
hence contradiction by A6; :: thesis: verum

end;

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

then X1 c= [:[:X2,X3:],X4,X5,X1:] by TH12;
hence contradiction by A2, MCART_1:63; :: thesis: verum

end;

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

then X1 c= [:[:X3,X4:],X5,X1,X2:] by TH12;
hence contradiction by A2, MCART_1:63; :: thesis: verum

end;

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

then X1 c= [:[:X4,X5:],X1,X2,X3:] by TH12;
hence contradiction by A2, MCART_1:63; :: thesis: verum

end;

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

consider x being set such that
A8: x in X1 and
A9: for x1, x2, x3, x4, x5 being set st ( x1 in X1 or x2 in X1 ) holds
x <> [x1,x2,x3,x4,x5] by A2, Th8;
reconsider x = x as Element of [:X5,X1,X2,X3,X4:] by A7, A8;
( x = [(x `1 ),(x `2 ),(x `3 ),(x `4 ),(x `5 )] & x `2 in X1 ) by A3, Th19;
hence contradiction by A9; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum