let a be set ; :: thesis: 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 ; :: thesis: ( 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:] ; :: thesis: ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2]
then consider x1, x2 being set such that
A1: x1 in X1 and
A2: x2 in X2 and
A3: a = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1 as Element of X1 by A1;
reconsider x2 = x2 as Element of X2 by A2;
take x1 ; :: thesis: ex x2 being Element of X2 st a = [x1,x2]
take x2 ; :: thesis: a = [x1,x2]
thus a = [x1,x2] by A3; :: thesis: verum