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] and
A2: [{v},z] in Trace f ; :: thesis: [{x},y] in Trace f
x = v by A1, ZFMISC_1:33;
hence [{x},y] in Trace f by A1, A2, ZFMISC_1:33; :: thesis: verum

end;

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