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

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