let i, j be 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

reconsider j = j as Element of NAT by ORDINAL1:def 12;

<*j*> in elementary_tree i by A2, TREES_1:28;

then A3: ex n being 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

assume that

A1: elementary_tree i c= elementary_tree j and

A2: i > j ; :: thesis: contradiction

reconsider j = j as Element of NAT by ORDINAL1:def 12;

<*j*> in elementary_tree i by A2, TREES_1:28;

then A3: ex n being 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