:: deftheorem Def3 defines binary BINTREE1:def 3 :
for IT being DecoratedTree holds
( IT is binary iff dom IT is binary );