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 Th6;
hence not t ^ <*0*> in T by A1, Def5; :: thesis: verum
end;
assume that
A2: not t ^ <*0*> in T and
A3: not t in Leaves T ; :: thesis: contradiction
consider q being FinSequence of NAT such that
A4: q in T and
A5: t is_a_proper_prefix_of q by A3, Def5;
t is_a_prefix_of q by A5;
then consider r being FinSequence such that
A6: q = t ^ r by Th1;
reconsider r = r as FinSequence of NAT by A6, FINSEQ_1:36;
len q = (len t) + (len r) by A6, FINSEQ_1:22;
then len r <> 0 by A5, Th5;
then r <> {} ;
then consider p being FinSequence of NAT , x being Element of NAT such that
A7: r = <*x*> ^ p by FINSEQ_2:130;
q = (t ^ <*x*>) ^ p by A6, A7, FINSEQ_1:32;
then t ^ <*x*> in T by A4, Th20;
hence contradiction by A2, Def3; :: thesis: verum