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
A3: <*j*> in elementary_tree i by A2, TREES_1:55;
A4: ex n being Element of NAT st
( n < j & <*j*> = <*n*> ) by A1, A3, TREES_1:57;
A5: <*j*> . 1 = j by FINSEQ_1:57;
thus contradiction by A4, A5, FINSEQ_1:57; :: thesis: verum