Actually, it seems that the current implementation checks whether the reverse order does not satisfy the property, and those are not equivalent, thus causing all this confusion.
That seems backwards to me. The fundamental concept is being sorted, while sorting is just any algorithm that causes a sequence to be sorted. This definition is at least much easier to explain. I get a bit of a headache trying to grasp the ‘inverse’ definition of the concepts, that you are advocating.