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 )

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 Nat : t ^ <*n*> in T } by TREES_2:def 5;

then consider n being 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

( 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 = {} )

set x = the Element of succ t;assume
succ t = {}
; :: thesis: t in Leaves T

then not t ^ <*0*> in { (t ^ <*n*>) where n is 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;then not t ^ <*0*> in { (t ^ <*n*>) where n is 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

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 Nat : t ^ <*n*> in T } by TREES_2:def 5;

then consider n being 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