let x, X, y, Y be set ; :: thesis: ( x in X & y in Y implies {[x,y]} is Relation of X,Y )
assume ( x in X & y in Y ) ; :: thesis: {[x,y]} is Relation of X,Y
then [x,y] in [:X,Y:] by ZFMISC_1:106;
hence {[x,y]} is Relation of X,Y by ZFMISC_1:37; :: thesis: verum