After "I_a", it is always the case that "b" holds.