let z, X, Y be set ; :: thesis: ( ex x, y being set st z = [x,y] & z `1 in X & z `2 in Y implies z in [:X,Y:] )
assume ex x, y being set st z = [x,y] ; :: thesis: ( not z `1 in X or not z `2 in Y or z in [:X,Y:] )
then [(z `1),(z `2)] = z by Th8;
hence ( not z `1 in X or not z `2 in Y or z in [:X,Y:] ) by ZFMISC_1:def 2; :: thesis: verum