theorem Th2: :: TREES_4:2

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