( I_KD <= I_FD & I_FD <= I_LK & I_LK <= I_WB ) by Lemma141, Lemma142, Lemma113;