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 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 ; :: thesis: ex y being Element of Y st z = [x,y]
take y ; :: thesis: z = [x,y]
thus z = [x,y] by A3; :: thesis: verum