Correctness of Deletion algorithm of BST in CLRS

It's not quite obvious to me why the algorithm (see below) to delete a node from a binary search tree, that CLRS offers, works correctly (like how do we know that the inorder arrangement of the nodes would be maintained in the correct manner ?); Is there any formal proof that could explain a bit more in depth about it? I would be really greatful if anyone could help me with this. The algorithm is as follows:

Deletion

The overall strategy for deleting a node z from a binary search tree T has three basic cases but, as we shall see, one of the cases is a bit tricky.

• If z has no children, then we simply remove it by modifying its parent to re- place z with NIL as its child.
• If z has just one child, then we elevate that child to take z’s position in the tree by modifying z’s parent to replace z by z’s child.
• If z has two children, then we find z’s successor y—which must be in z’s right subtree—and have y take z’s position in the tree. The rest of z’s original right subtree becomes y’s new right subtree, and z’s left subtree becomes y’s new left subtree. This case is the tricky one because, as we shall see, it matters whether y is z’s right child.

I have tried to prove it by analys of case by case but that seems to hard.

BST is defined by the following property: for each node N, all nodes in the left subtree of N are smaller than N, and all nodes in the right subtree of N are larger than N. Note this does not admit any duplicates in the tree.

In case 1 of the algorithm, subtrees of every node either do not change or lose a node, so the property is kept intact.

The same is true about case 2.

In case 3, we need to show that the property holds for the newly formed tree with the root of y and its subtrees. The procedure has three steps: (a) remove y and (b) replace x with y (c) copy y into the node z. Step (a) works just like case 1 or 2 above, so the property still holds (note y cannot have a left child). Step (b) doesn't violate the property either since no nodes exist between x and y. The trickiness of the case doesn't bleed into the proof. Step (c) holds the BST property as well; since y is greater than the original z (which means greater than the whole left subtree rooted at original z), but also smaller than the rest of the right subtree of the original z (excluding y itself), because it's in the left subtree rooted at right child of original z. so what we have done is consistent with the properties we have defined so far.