subtype example backwards?

I've recently retired, and hope to use Z3 for a project. So I'm trying to catch up on this amazing tool. In the process, I was reading https://microsoft.github.io/z3guide/docs/logic/Quantifiers#effectively-propositional, and I got confused. It says:

The following example axiomatizes a subtype partial order relation that has the tree property. That is, if x and y are subtypes of z, then x is a subtype of y or y is a subtype of x.

I understand the term "subtype" to mean that in a language with single inheritance, if B inherits from A, then B is a (proper) subtype of A, and A is a supertype of B. So I think this sentence (and the example that follows it) is reversed -- it would make sense if you substituted "supertype" for "subtype". To make this point clearly, if B1 and B2 both inherit from A, then they are both subtypes of A, but neither of B1 or B2 are subtypes (or supertypes) of the other.

Open the linked Z3 Guide Quantifiers page and inspect the “Effectively propositional” subsection, including the subtype example. Check the terminology and example against the inheritance interpretation described in the issue; done means the wording and example consistently describe the intended partial-order relation.