theorem Th83: :: ZFMISC_1:84

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