consider y being Element of Y;
consider x being Element of X;
[x,y] in [:the carrier of X,the carrier of Y:] by ZFMISC_1:106;
hence not [:X,Y:] is empty by Def2; :: thesis: verum