let X, Y, A be set ; :: thesis: 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 ; :: thesis: ( 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:] ) ; :: thesis: ex x being Element of X ex y being Element of Y st z = [x,y]
then consider x, y being set such that
A1: ( x in X & y in Y & z = [x,y] ) by ZFMISC_1:103;
reconsider x = x as Element of X by A1;
reconsider y = y as Element of Y by A1;
take x ; :: thesis: ex y being Element of Y st z = [x,y]
take y ; :: thesis: z = [x,y]
thus z = [x,y] by A1; :: thesis: verum