for X, Y, A, 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]