let i, j be Element of NAT ; :: thesis: ( elementary_tree i c= elementary_tree j implies i <= j )
assume that
A1: elementary_tree i c= elementary_tree j and
A2: i > j ; :: thesis: contradiction
<*j*> in elementary_tree i by A2, TREES_1:55;
then A4: ex n being Element of NAT st
( n < j & <*j*> = <*n*> ) by A1, TREES_1:57;
<*j*> . 1 = j by FINSEQ_1:57;
hence contradiction by A4, FINSEQ_1:57; :: thesis: verum