theorem Th24: :: RELSET_2:24

for y being object
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)