:: deftheorem defines = TREES_4:def 1 :
for T1, T2 being DecoratedTree holds
( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) );