let x, y be object ; :: thesis: for X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )
let X, Y be set ; :: thesis: ( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )
thus ( [x,y] in [:X,Y:] implies ( x in X & y in Y ) ) :: thesis: ( x in X & y in Y implies [x,y] in [:X,Y:] )

proof

assume [x,y] in [:X,Y:] ; :: thesis: ( x in X & y in Y )
then ex x1, y1 being object st
( x1 in X & y1 in Y & [x,y] = [x1,y1] ) by Def2;
hence ( x in X & y in Y ) by XTUPLE_0:1; :: thesis: verum

end;

thus ( x in X & y in Y implies [x,y] in [:X,Y:] ) by Def2; :: thesis: verum