Definition 1.55 includes this sentence: "A monotone function \$$f: P \to Q\$$ is called an *isomorphism* if there exists a monotone function \$$g: Q \to P\$$ such that \$$f.g = id_P\$$ and \$$g.f = id_Q\$$.” (Here \$$P\$$ and \$$Q\$$ are preorders each with its own ordering).

Question: Is the “and…” part redundant? It seems that \$$g.f = id_Q\$$ is implied by what precedes it.