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:28;
then A3: ex n being Element of NAT st
( n < j & <*j*> = <*n*> ) by A1, TREES_1:30;
<*j*> . 1 = j by FINSEQ_1:40;
hence contradiction by A3, FINSEQ_1:40; :: thesis: verum