theorem :: RELSET_1:3

for X, Y being set
for x, y being object st x in X & y in Y holds
{[x,y]} is Relation of X,Y by ZFMISC_1:31, ZFMISC_1:87;