:: deftheorem defines binary BINTREE1:def 2 :
for IT being Tree holds
( IT is binary iff for t being Element of IT st not t in Leaves IT holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)} );