:: deftheorem Def19 defines LinTrace COHSP_1:def 19 :
for f being Function
for b₂ being set holds
( b₂ = LinTrace f iff for x being object holds
( x in b₂ iff ex y, z being object st
( x = [y,z] & [{y},z] in Trace f ) ) );