set N = N_CC ;
N_CC is decreasing ;
hence ex b₁ being Fuzzy_Negation st b₁ is decreasing ; :: thesis: verum