consider x4 being set such that
A1: x4 in X4 by XBOOLE_0:def 1;
consider x123 being set such that
A2: x123 in [:X1,X2,X3:] by XBOOLE_0:def 1;
[x123,x4] in [:[:X1,X2,X3:],X4:] by A2, A1, ZFMISC_1:def 2;
hence not [:X1,X2,X3,X4:] is empty by ZFMISC_1:def 4; :: thesis: verum