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