let a be set ; :: thesis: for X1, X2, X3, X4 being non empty set holds
( a in [:X1,X2,X3,X4:] 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] )
let X1, X2, X3, X4 be non empty set ; :: thesis: ( a in [:X1,X2,X3,X4:] 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] )
thus ( a in [:X1,X2,X3,X4:] implies 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: ( 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 a in [:X1,X2,X3,X4:] )

proof

assume a in [:X1,X2,X3,X4:] ; :: thesis: 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]
then a in [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
then consider x123, x4 being object such that
A1: x123 in [:X1,X2,X3:] and
A2: x4 in X4 and
A3: a = [x123,x4] by ZFMISC_1:def 2;
reconsider x4 = x4 as Element of X4 by A2;
consider x1 being Element of X1, x2 being Element of X2, x3 being Element of X3 such that
A4: x123 = [x1,x2,x3] by A1, Th3;
a = [x1,x2,x3,x4] by A3, A4;
hence 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: verum

end;

given x1 being Element of X1, x2 being Element of X2, x3 being Element of X3, x4 being Element of X4 such that A5: a = [x1,x2,x3,x4] ; :: thesis: a in [:X1,X2,X3,X4:]
a = [[x1,x2,x3],x4] by A5;
then a in [:[:X1,X2,X3:],X4:] ;
hence a in [:X1,X2,X3,X4:] by ZFMISC_1:def 4; :: thesis: verum