set g = N_CC ;
T0: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
then T1: N_CC . 0 = 1 - 0 by NDef
.= 1 ;
a1: N_CC . 1 = 1 - 1 by T0, NDef
.= 0 ;
for a, b being Element of [.0,1.] st a <= b holds
N_CC . a >= N_CC . b
proof
let a, b be Element of [.0,1.]; :: thesis: ( a <= b implies N_CC . a >= N_CC . b )
assume Y0: a <= b ; :: thesis: N_CC . a >= N_CC . b
( N_CC . a = 1 - a & N_CC . b = 1 - b ) by NDef;
hence N_CC . a >= N_CC . b by Y0, XREAL_1:13; :: thesis: verum
end;
hence ( N_CC is satisfying_(N1) & N_CC is satisfying_(N2) ) by a1, NonInc, T1; :: thesis: verum