theorem IRSIsLCP: :: FUZIMPL4:27

I_RS is N_CC -satisfying_L-CP