let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in LinTrace f or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in LinTrace f ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then ex y, z being object st
( x = [y,z] & [{y},z] in Trace f ) by Def19;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum