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

now

given v, z being set such that A1: ( [x,y] = [v,z] & [{v},z] in Trace f ) ; :: thesis: [{x},y] in Trace f
( x = v & y = z ) by A1, ZFMISC_1:33;
hence [{x},y] in Trace f by A1; :: thesis: verum

end;

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