for X, x, y being set
for R being Relation of X st x,y in R holds
( x in X & y in X ) by ZFMISC_1:87;