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;

assume t in Leaves T ; :: thesis: succ t = {}
then A1: not t ^ <*0 *> in T by TREES_1:91;
assume A2: succ t <> {} ; :: thesis: contradiction
consider x being Element of succ t;
x in succ t by A2;
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
A3: ( x = t ^ <*n*> & t ^ <*n*> in T ) ;
0 <= n by NAT_1:2;
hence contradiction by A1, A3, TREES_1:def 5; :: thesis: verum