take N_CC ; :: thesis: N_CC is negation-strong
thus N_CC is negation-strong ; :: thesis: verum