take I_LK ; :: thesis: ( I_LK is satisfying_(NP) & I_LK is satisfying_(OP) & I_LK is satisfying_(EP) & I_LK is satisfying_(IP) )
thus ( I_LK is satisfying_(NP) & I_LK is satisfying_(OP) & I_LK is satisfying_(EP) & I_LK is satisfying_(IP) ) ; :: thesis: verum