let x, y be object ; for X, Y being set holds
( [x,y] in [:X,Y:] iff ( x in X & y in Y ) )
let X, Y be set ; ( [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 ) )
( x in X & y in Y implies [x,y] in [:X,Y:] )
thus
( x in X & y in Y implies [x,y] in [:X,Y:] )
by Def2; verum