theorem Th42: :: RELAT_1:48

for X being set
for x, y being object
for R being Relation holds
( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )