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 object 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:3; :: thesis: verum