theorem :: FUZIMPL2:11
( I_RS <= I_GD & I_GD <= I_FD & I_FD <= I_LK & I_LK <= I_WB ) by Lemma151, Lemma152, Lemma153, Lemma113;