let T be Tree; :: thesis: ( ( for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) implies T is binary )
assume for t being Element of T holds succ t = {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: T is binary
then for t being Element of T st not t in Leaves T holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)} ;
hence T is binary by BINTREE1:def 2; :: thesis: verum