let D, X1, X2, X3 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 st a = [x1,x2,x3] ) ) implies D = [:X1,X2,X3:] )
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 st a = [x1,x2,x3] )
; D = [:X1,X2,X3:]
now for a being object holds
( ( a in D implies a in [:[:X1,X2:],X3:] ) & ( a in [:[:X1,X2:],X3:] implies a in D ) )let a be
object ;
( ( a in D implies a in [:[:X1,X2:],X3:] ) & ( a in [:[:X1,X2:],X3:] implies a in D ) )thus
(
a in D implies
a in [:[:X1,X2:],X3:] )
( a in [:[:X1,X2:],X3:] implies a in D )proof
assume
a in D
;
a in [:[:X1,X2:],X3:]
then consider x1 being
Element of
X1,
x2 being
Element of
X2,
x3 being
Element of
X3 such that A2:
a = [x1,x2,x3]
by A1;
a = [[x1,x2],x3]
by A2;
hence
a in [:[:X1,X2:],X3:]
;
verum
end; assume
a in [:[:X1,X2:],X3:]
;
a in Dthen consider x12,
x3 being
object such that A3:
x12 in [:X1,X2:]
and A4:
x3 in X3
and A5:
a = [x12,x3]
by ZFMISC_1:def 2;
reconsider x3 =
x3 as
Element of
X3 by A4;
consider x1,
x2 being
object such that A6:
x1 in X1
and A7:
x2 in X2
and A8:
x12 = [x1,x2]
by A3, ZFMISC_1:def 2;
reconsider x2 =
x2 as
Element of
X2 by A7;
reconsider x1 =
x1 as
Element of
X1 by A6;
a = [x1,x2,x3]
by A5, A8;
hence
a in D
by A1;
verum end;
then
D = [:[:X1,X2:],X3:]
by TARSKI:2;
hence
D = [:X1,X2,X3:]
by ZFMISC_1:def 3; verum