( I_KD <= I_RC & I_RC <= I_LK & I_LK <= I_WB ) by Lemma111, Lemma112, Lemma113;