take N_CC ; :: thesis: N_CC is negation-strict
( N_CC is satisfying_(N3) & N_CC is satisfying_(N4) ) by FUZIMPL3:def 9, FUZIMPL3:def 10;
hence N_CC is negation-strict by FUZIMPL3:def 12; :: thesis: verum