let z be object ; :: thesis: for X, Y being set st z in [:X,Y:] holds
( z `1 in X & z `2 in Y )
let X, Y be set ; :: thesis: ( z in [:X,Y:] implies ( z `1 in X & z `2 in Y ) )
assume z in [:X,Y:] ; :: thesis: ( z `1 in X & z `2 in Y )
then consider x, y being object such that
A1: ( x in X & y in Y & z = [x,y] ) by ZFMISC_1:def 2;
thus ( z `1 in X & z `2 in Y ) by A1; :: thesis: verum