let z, X, Y be set ; :: thesis: ( z in [:X,Y:] implies ex x, y being set st [x,y] = z )
assume z in [:X,Y:] ; :: thesis: ex x, y being set st [x,y] = z
then ex x, y being set st
( x in X & y in Y & [x,y] = z ) by Def2;
hence ex x, y being set st [x,y] = z ; :: thesis: verum