let T be Tree; :: thesis: ( ( for t being Element of T holds succ t = {(t ^ <*0 *>),(t ^ <*1*>)} ) implies Leaves T = {} )
assume A1: for t being Element of T holds succ t = {(t ^ <*0 *>),(t ^ <*1*>)} ; :: thesis: Leaves T = {}
assume Leaves T <> {} ; :: thesis: contradiction
then consider x being set such that
A2: x in Leaves T by XBOOLE_0:def 1;
reconsider t = x as Element of T by A2;
succ t = {(t ^ <*0 *>),(t ^ <*1*>)} by A1;
hence contradiction by A2, BINTREE1:5; :: thesis: verum