:: deftheorem Def17 defines Trace COHSP_1:def 17 :
for f being Function
for b₂ being set holds
( b₂ = Trace f iff for x being set holds
( x in b₂ iff 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 ) ) ) );