theorem Th52: :: COHSP_1:52

for f being Function
for x, y being object st [x,y] in LinTrace f holds
( {x} in dom f & y in f . {x} )