theorem Th11: :: DOMAIN_1:11

for D, X1, X2, X3, X4 being non empty set st ( 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 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) holds
D = [:X1,X2,X3,X4:]