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

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