theorem Th5: :: EXCHSORT:5

for f being Function
for r being Relation
for x being object holds
( x in f .: r iff ex y, z being object st
( [y,z] in r & [y,z] in dom f & f . (y,z) = x ) )