:: deftheorem Def4 defines binary BINTREE1:def 4 :
for IT being non empty DTConstrStr holds
( IT is binary iff for s being Symbol of IT
for p being FinSequence st s ==> p holds
ex x1, x2 being Symbol of IT st p = <*x1,x2*> );