let D, X1, X2, X3, X4 be non empty set ; :: thesis: ( ( 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] ) ) implies D = [:X1,X2,X3,X4:] )
assume A1: 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] ) ; :: thesis: D = [:X1,X2,X3,X4:]

now :: thesis: for a being object holds
( ( a in D implies a in [:[:X1,X2,X3:],X4:] ) & ( a in [:[:X1,X2,X3:],X4:] implies a in D ) )

let a be object ; :: thesis: ( ( a in D implies a in [:[:X1,X2,X3:],X4:] ) & ( a in [:[:X1,X2,X3:],X4:] implies a in D ) )
thus ( a in D implies a in [:[:X1,X2,X3:],X4:] ) :: thesis: ( a in [:[:X1,X2,X3:],X4:] implies a in D )

proof

assume a in D ; :: thesis: a in [:[:X1,X2,X3:],X4:]
then consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3, x4 being Element of X4 such that
A2: a = [x1,x2,x3,x4] by A1;
a = [[x1,x2,x3],x4] by A2;
hence a in [:[:X1,X2,X3:],X4:] ; :: thesis: verum

end;

assume a in [:[:X1,X2,X3:],X4:] ; :: thesis: a in D
then consider x123, x4 being object such that
A3: x123 in [:X1,X2,X3:] and
A4: x4 in X4 and
A5: a = [x123,x4] by ZFMISC_1:def 2;
reconsider x4 = x4 as Element of X4 by A4;
consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that
A6: x123 = [x1,x2,x3] by A3, Th3;
a = [x1,x2,x3,x4] by A5, A6;
hence a in D by A1; :: thesis: verum

end;

then D = [:[:X1,X2,X3:],X4:] by TARSKI:2;
hence D = [:X1,X2,X3,X4:] by ZFMISC_1:def 4; :: thesis: verum