( x in X & y in Y ) by Def1;
hence In ([x,y],[:X,Y:]) = [x,y] by Def7, ZFMISC_1:87; :: thesis: verum