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