( I_RC <= I_LK & I_LK <= I_WB ) by Lemma132, Lemma113;