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

end;

set x = the Element of succ t;
assume t in Leaves T ; :: thesis: succ t = {}
then A1: not t ^ <*0*> in T by TREES_1:54;
assume succ t <> {} ; :: thesis: contradiction
then the Element of succ t in succ t ;
then the Element of succ t 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
the Element of succ t = t ^ <*n*> and
A2: t ^ <*n*> in T ;
0 <= n by NAT_1:2;
hence contradiction by A1, A2, TREES_1:def 3; :: thesis: verum