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

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