take N_CC ; :: thesis: ( N_CC is satisfying_(N1) & N_CC is satisfying_(N2) )
thus ( N_CC is satisfying_(N1) & N_CC is satisfying_(N2) ) ; :: thesis: verum