let p be FinSequence; :: thesis: ( p is Tree-yielding implies elementary_tree (len p) c= tree p )
assume A1: p is Tree-yielding ; :: thesis: elementary_tree (len p) c= tree p
then A2: ( rng p is constituted-Trees & ( for n being Element of NAT
for q being FinSequence st n < len p & q in p . (n + 1) holds
<*n*> ^ q in tree p ) ) by Def9, Def15;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in elementary_tree (len p) or q in tree p )
assume q in elementary_tree (len p) ; :: thesis: q in tree p
then ( q in { <*n*> where n is Element of NAT : n < len p } or q in {{} } ) by XBOOLE_0:def 3;
then A3: ( ex n being Element of NAT st
( q = <*n*> & n < len p ) or q = {} ) by TARSKI:def 1;
assume A4: not q in tree p ; :: thesis: contradiction
then consider n being Element of NAT such that
A5: ( q = <*n*> & n < len p ) by A3, TREES_1:47;
p . (n + 1) in rng p by A5, Lm4;
then reconsider t = p . (n + 1) as Tree by A2, Def3;
( {} in t & <*n*> ^ {} = q ) by A5, FINSEQ_1:47, TREES_1:47;
hence contradiction by A1, A4, A5, Def15; :: thesis: verum