Three words: The Sequential Access Theorem.
http://www.wseas.us/e-library/conferences/cairns2001/papers/632.pdf
Because the above loop repeatedly removes the maximum value, it effectively visits all of the elements in sequence, and so I'm pretty certain the sequential access theorem applies.