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 A5: t = t ^ <*n*> by A3, XBOOLE_0:def 8;
t = t ^ {} by FINSEQ_1:47;
hence contradiction by A5, FINSEQ_1:46; :: thesis: verum

end;

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