theorem :: DOMAIN_1:19

for X1, X2 being non empty set holds [:X1,X2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum }