let T be Tree; :: thesis: for t being Element of T holds
( t in Leaves T iff for n being Element of NAT holds not t ^ <*n*> in T )
let t be Element of T; :: thesis: ( t in Leaves T iff for n being Element of NAT holds not t ^ <*n*> in T )

hereby :: thesis: ( ( for n being Element of NAT holds not t ^ <*n*> in T ) implies t in Leaves T )

assume A1: t in Leaves T ; :: thesis: for n being Element of NAT holds not t ^ <*n*> in T
given n being Element of NAT such that A2: t ^ <*n*> in T ; :: thesis: contradiction
A3: not t is_a_proper_prefix_of t ^ <*n*> by A1, A2, Def8;
t is_a_prefix_of t ^ <*n*> by Th8;
then A4: t = t ^ <*n*> by A3, XBOOLE_0:def 8;
t = t ^ {} by FINSEQ_1:34;
hence contradiction by A4, FINSEQ_1:33; :: thesis: verum

end;

assume that
A5: for n being Element of NAT holds not t ^ <*n*> in T and
A6: not t in Leaves T ; :: thesis: contradiction
consider q being FinSequence of NAT such that
A7: q in T and
A8: t is_a_proper_prefix_of q by A6, Def8;
t is_a_prefix_of q by A8, XBOOLE_0:def 8;
then consider r being FinSequence such that
A9: q = t ^ r by Th8;
reconsider r = r as FinSequence of NAT by A9, FINSEQ_1:36;
len q = (len t) + (len r) by A9, FINSEQ_1:22;
then len r <> 0 by A8, Th24;
then r <> {} ;
then consider p being FinSequence of NAT , x being Element of NAT such that
A10: r = <*x*> ^ p by FINSEQ_2:130;
reconsider x = x as Element of NAT ;
q = (t ^ <*x*>) ^ p by A9, A10, FINSEQ_1:32;
hence contradiction by A5, A7, Th46; :: thesis: verum