theorem Th1: :: TREES_4:1

for i, j being Nat st elementary_tree i c= elementary_tree j holds
i <= j