:: deftheorem defines Root MODAL_1:def 2 :
for D being non empty set
for T being DecoratedTree of D holds Root T = T . (Root (dom T));