theorem Th4: :: MMLQUER2:4

for X being set
for R being Relation
for x, y being set holds
( [x,y] in R |_2 X iff ( x in X & y in X & [x,y] in R ) )