let s, t be Tree; not {} in Leaves (tree (t,s))
assume A1:
{} in Leaves (tree (t,s))
; contradiction
set q = <*t,s*>;
<*t,s*> . 1 = t
by FINSEQ_1:44;
then
( 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 )
then
<*0*> in elementary_tree 0
by A2;
hence
contradiction
by TARSKI:def 1, TREES_1:29; verum