:: deftheorem defines repr_of PRELAMB:def 11 :
for s being non empty typealg
for x being type of s st s is free holds
for b₃ being finite DecoratedTree of the carrier of s holds
( b₃ = repr_of x iff for Tr being finite DecoratedTree of the carrier of s holds
( Tr represents x iff b₃ = Tr ) );