let X, Y, A be set ; for z being set st z in A & A c= [:X,Y:] holds
ex x being Element of X ex y being Element of Y st z = [x,y]
let z be set ; ( z in A & A c= [:X,Y:] implies ex x being Element of X ex y being Element of Y st z = [x,y] )
assume
( z in A & A c= [:X,Y:] )
; ex x being Element of X ex y being Element of Y st z = [x,y]
then consider x, y being object such that
A1:
x in X
and
A2:
y in Y
and
A3:
z = [x,y]
by ZFMISC_1:84;
reconsider x = x, y = y as set by TARSKI:1;
reconsider y = y as Element of Y by A2, Def1;
reconsider x = x as Element of X by A1, Def1;
take
x
; ex y being Element of Y st z = [x,y]
take
y
; z = [x,y]
thus
z = [x,y]
by A3; verum