Эффективное постусловие Эйфеля для обеспечения сортировки массива

Я реализовал запрос, который сообщает, отсортирован ли массив или нет. Я хочу сделать хорошее постусловие, которое будет эффективно проверять, отсортирован ли массив с помощью across или чего-то еще.

Я пытался сделать это так:

is_sorted (a: ARRAY [INTEGER]): BOOLEAN
        -- Given an array, tell if it's sorted in ascending order
    require
        array_set: a /= Void
    local
        i, j, temp: INTEGER
    do
        Result := True

        from
            i := a.lower
            j := i + 1
        invariant
            (i >= a.lower) and (i <= a.upper)
        until
            i = (a.upper) or (Result = False)
        loop
            if a[i] > a[j] then
                Result := False
            end

            i := i + 1
            j := j + 1
        variant
            a.count - i + 1
        end -- End of loop

    ensure
          -- Check if ARRAY is sorted here
    end

Я пытался написать что-то вроде этого:

ensure
    across a as el all (el.item <= el.forth.item) end

Но это явно не работает, потому что el.forth — это не запрос, а команда.

Как я могу заставить это across работать или я должен сделать что-то еще?