let x be object ; :: thesis: for X, Y being set st x in [:X,Y:] holds
x is pair
let X, Y be set ; :: thesis: ( x in [:X,Y:] implies x is pair )
assume x in [:X,Y:] ; :: thesis: x is pair
then ex a, b being object st
( a in X & b in Y & x = [a,b] ) by ZFMISC_1:def 2;
hence x is pair ; :: thesis: verum