The second logical implication was made the whole property holding
when the part after the 1st implication didn't hold. So, the 2nd
implication is replaced by an and in combination with the next
operator. Now the property fails when one of the two and'ed parts after
the implication fails.