theorem Th76: :: GLUNIR00:76

for V being non empty set
for E being Relation of V
for X, Y being set holds (Y |` E) | X = (createGraph (V,E)) .edgesDBetween (X,Y)