let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in Trace f or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in Trace f ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then ex a, y being set st
( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) by Def17;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum