let s, t be Tree; :: thesis: not {} in Leaves (tree (t,s))
assume A1: {} in Leaves (tree (t,s)) ; :: thesis: contradiction
set q = <*t,s*>;
( 0 < len <*t,s*> & {} in <*t,s*> . (0 + 1) ) by TREES_1:22;
then <*0*> ^ {} in tree (t,s) by TREES_3:def 15;
then A2: <*0*> in tree (t,s) by FINSEQ_1:34;
for p being object holds
( p in tree (t,s) iff p in elementary_tree 0 )

proof

let p0 be object ; :: thesis: ( p0 in tree (t,s) iff p0 in elementary_tree 0 )

hereby :: thesis: ( p0 in elementary_tree 0 implies p0 in tree (t,s) )

assume that
A3: p0 in tree (t,s) and
A4: not p0 in elementary_tree 0 ; :: thesis: contradiction
reconsider p = p0 as FinSequence of NAT by A3, TREES_1:19;
p <> {} by A4, TARSKI:def 1, TREES_1:29;
then consider q being FinSequence of NAT , n being Element of NAT such that
A5: p = <*n*> ^ q by FINSEQ_2:130;
{} ^ <*n*> = <*n*> by FINSEQ_1:34;
hence contradiction by A1, TREES_1:55, A3, A5, TREES_1:21; :: thesis: verum

end;

assume p0 in elementary_tree 0 ; :: thesis: p0 in tree (t,s)
then p0 = {} by TARSKI:def 1, TREES_1:29;
hence p0 in tree (t,s) by TREES_1:22; :: thesis: verum

end;

then <*0*> in elementary_tree 0 by A2;
hence contradiction by TARSKI:def 1, TREES_1:29; :: thesis: verum