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