let T be Tree; :: thesis: for t being Element of T holds
( succ t = {} iff t in Leaves T )
let t be Element of T; :: thesis: ( succ t = {} iff t in Leaves T )

hereby :: thesis: ( t in Leaves T implies succ t = {} )

assume succ t = {} ; :: thesis: t in Leaves T
then not t ^ <*0*> in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by TREES_2:def 5;
then not t ^ <*0*> in T ;
hence t in Leaves T by TREES_1:91; :: thesis: verum

end;

consider x being Element of succ t;
assume t in Leaves T ; :: thesis: succ t = {}
then A1: not t ^ <*0*> in T by TREES_1:91;
assume succ t <> {} ; :: thesis: contradiction
then x in succ t ;
then x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by TREES_2:def 5;
then consider n being Element of NAT such that
x = t ^ <*n*> and
A2: t ^ <*n*> in T ;
0 <= n by NAT_1:2;
hence contradiction by A1, A2, TREES_1:def 5; :: thesis: verum