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

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

assume A1: t in Leaves T ; :: thesis: for n being Nat holds not t ^ <*n*> in T
given n being Nat such that A2: t ^ <*n*> in T ; :: thesis: contradiction
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A3: not t is_a_proper_prefix_of t ^ <*nn*> by A1, A2, Def5;
t is_a_prefix_of t ^ <*n*> by Th1;
then A4: t = t ^ <*n*> by A3;
t = t ^ {} by FINSEQ_1:34;
hence contradiction by A4, FINSEQ_1:33; :: thesis: verum

end;

assume that
A5: for n being 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, Def5;
t is_a_prefix_of q by A8;
then consider r being FinSequence such that
A9: q = t ^ r by Th1;
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, Th5;
then r <> {} ;
then consider p being FinSequence of NAT , x being Element of NAT such that
A10: r = <*x*> ^ p by FINSEQ_2:130;
q = (t ^ <*x*>) ^ p by A9, A10, FINSEQ_1:32;
hence contradiction by A5, A7, Th20; :: thesis: verum