theorem Th1: :: FUNCT_4:1

for Z being set st ( for z being object st z in Z holds
ex x, y being object st z = [x,y] ) holds
ex X, Y being set st Z c= [:X,Y:]