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
A2: t is_a_proper_prefix_of t ^ <*0 *> by Th30;
thus not t ^ <*0 *> in T by A1, A2, 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;
A7: t is_a_prefix_of q by A6, XBOOLE_0:def 8;
consider r being FinSequence such that
A8: q = t ^ r by A7, Th8;
reconsider r = r as FinSequence of NAT by A8, FINSEQ_1:50;
A9: len q = (len t) + (len r) by A8, FINSEQ_1:35;
A10: len r <> 0 by A6, A9, Th24;
A11: r <> {} by A10;
consider p being FinSequence of NAT , x being Nat such that
A12: r = <*x*> ^ p by A11, FINSEQ_2:150;
reconsider x = x as Element of NAT by ORDINAL1:def 13;
A13: q = (t ^ <*x*>) ^ p by A8, A12, FINSEQ_1:45;
A14: t ^ <*x*> in T by A5, A13, Th46;
thus contradiction by A3, A14, Def5; :: thesis: verum