theorem Th43: :: RELAT_1:49

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