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