:: deftheorem defines root-label BINTREE1:def 1 :
for D being non empty set
for t being DecoratedTree of D holds root-label t = t . {};