:: deftheorem Def2 defines [: ZFMISC_1:def 2 :
for X1, X2, b₃ being set holds
( b₃ = [:X1,X2:] iff for z being object holds
( z in b₃ iff ex x, y being object st
( x in X1 & y in X2 & z = [x,y] ) ) );