let a be set ; for X1, X2 being non empty set st a in [:X1,X2:] holds
ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2]
let X1, X2 be non empty set ; ( a in [:X1,X2:] implies ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2] )
assume
a in [:X1,X2:]
; ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2]
then consider x1, x2 being object such that
A1:
x1 in X1
and
A2:
x2 in X2
and
A3:
a = [x1,x2]
by ZFMISC_1:def 2;
reconsider x2 = x2 as Element of X2 by A2;
reconsider x1 = x1 as Element of X1 by A1;
take
x1
; ex x2 being Element of X2 st a = [x1,x2]
take
x2
; a = [x1,x2]
thus
a = [x1,x2]
by A3; verum