let z, 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 set such that
W: ( x in X & y in Y & z = [x,y] ) by ZFMISC_1:def 2;
( [x,y] `1 = x & [x,y] `2 = y ) ;
hence ( z `1 in X & z `2 in Y ) by W; :: thesis: verum