let a be set ; :: thesis: for X1, X2, X3 being non empty set holds
( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] )
let X1, X2, X3 be non empty set ; :: thesis: ( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] )
thus ( a in [:X1,X2,X3:] implies ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) :: thesis: ( ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] implies a in [:X1,X2,X3:] )

proof

assume a in [:X1,X2,X3:] ; :: thesis: ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3]
then a in [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
then consider x12, x3 being object such that
A1: x12 in [:X1,X2:] and
A2: x3 in X3 and
A3: a = [x12,x3] by ZFMISC_1:def 2;
reconsider x3 = x3 as Element of X3 by A2;
consider x1, x2 being object such that
A4: x1 in X1 and
A5: x2 in X2 and
A6: x12 = [x1,x2] by A1, ZFMISC_1:def 2;
reconsider x2 = x2 as Element of X2 by A5;
reconsider x1 = x1 as Element of X1 by A4;
a = [x1,x2,x3] by A3, A6;
hence ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ; :: thesis: verum

end;

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