theorem :: FUZIMPL2:8

( I_RS <= I_GD & I_GD <= I_GG & I_GG <= I_LK & I_LK <= I_WB ) by Lemma121, Lemma122, Lemma123, Lemma113;