IC in dom p by Def16;
hence K: IC in dom (NPP p) by Th179; :: according to COMPOS_1:def 16 :: thesis: IC (NPP p) = l
IC p = l by Def16;
hence IC (NPP p) = l by K, GRFUNC_1:8; :: thesis: verum