How does implies work in Eiffel?

Question

Programming

I need to understand how implies works in the Eiffel programming language .
Reading the book "Feel the class" by Bertrand Mayer and it seems to me that the author has a contradictory code in the book. Here is an example:

ensure
  at_first : (not is_empty) implies (index=1)

Let me remind you the work implies: "The value of the boolean expression a implies b is true except if a is true and b false " took in article 8 DESIGN BY CONTRACT TM , ASSERTIONS, EXCEPTIONS
And now let's take the sentence:
"Now, in fact, the list is empty and the index equals 5", then
* not is_empty gives False
* index = 1 gives False
according to the truth table we get:
* at_first = True
But how can this be?