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

hereby :: thesis: ( not t ^ <*0 *> in T implies t in Leaves T )

assume A1: t in Leaves T ; :: thesis: not t ^ <*0 *> in T
t is_a_proper_prefix_of t ^ <*0 *> by Th30;
hence not t ^ <*0 *> in T by A1, Def8; :: thesis: verum

end;

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