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 ex x, y being set st
( x in X & y in Y & z = [x,y] ) by ZFMISC_1:def 2;
hence ( z `1 in X & z `2 in Y ) by Def1, Def2; :: thesis: verum