set y = the Element of Y;
set x = the Element of X;
[ the Element of X, the Element of Y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;
hence not [:X,Y:] is empty by Def2; :: thesis: verum