let D, X1, X2, X3, X4 be non empty set ; ( ( 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] )
; D = [:X1,X2,X3,X4:]
now 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 ;
( ( 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:] )
( a in [:[:X1,X2,X3:],X4:] implies a in D )proof
assume
a in D
;
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:]
;
verum
end; assume
a in [:[:X1,X2,X3:],X4:]
;
a in Dthen 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;
verum end;
then
D = [:[:X1,X2,X3:],X4:]
by TARSKI:2;
hence
D = [:X1,X2,X3,X4:]
by ZFMISC_1:def 4; verum