theorem :: DOMAIN_1:5

for D, X1, X2, X3 being non empty set holds
( D = [:X1,X2,X3:] iff for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) by Th3, Th4;