take f = N_CC ; :: thesis: ( f is bijective & f is decreasing )
thus ( f is bijective & f is decreasing ) ; :: thesis: verum