let f be Function; :: thesis: for x, y being object holds
( [x,y] in LinTrace f iff [{x},y] in Trace f )
let x, y be object ; :: thesis: ( [x,y] in LinTrace f iff [{x},y] in Trace f )

now :: thesis: ( ex v, z being object st
( [x,y] = [v,z] & [{v},z] in Trace f ) implies [{x},y] in Trace f )

given v, z being object such that A1: [x,y] = [v,z] and
A2: [{v},z] in Trace f ; :: thesis: [{x},y] in Trace f
x = v by A1, XTUPLE_0:1;
hence [{x},y] in Trace f by A1, A2, XTUPLE_0:1; :: thesis: verum

end;

hence ( [x,y] in LinTrace f iff [{x},y] in Trace f ) by Def19; :: thesis: verum