theorem Th50: :: COHSP_1:50

for f being Function
for x, y being object holds
( [x,y] in LinTrace f iff [{x},y] in Trace f )