theorem Th51: :: COHSP_1:51

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