set CN = ConjNeg (N,h);
AA: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
then A0: (ConjNeg (N,h)) . 0 = (h ") . (N . (h . 0)) by CNDef
.= (h ") . (N . 0) by LemmaBound
.= (h ") . 1 by N1Def
.= 1 by LemmaBound ;
A1: (ConjNeg (N,h)) . 1 = (h ") . (N . (h . 1)) by AA, CNDef
.= (h ") . (N . 1) by LemmaBound
.= (h ") . 0 by N1Def
.= 0 by LemmaBound ;
for a, b being Element of [.0,1.] st a <= b holds
(ConjNeg (N,h)) . a >= (ConjNeg (N,h)) . b

proof

let a, b be Element of [.0,1.]; :: thesis: ( a <= b implies (ConjNeg (N,h)) . a >= (ConjNeg (N,h)) . b )
assume a <= b ; :: thesis: (ConjNeg (N,h)) . a >= (ConjNeg (N,h)) . b
then h . a <= h . b by Rosnie;
then B1: N . (h . a) >= N . (h . b) by N2Def, NonInc;
B2: (ConjNeg (N,h)) . a = (h ") . (N . (h . a)) by CNDef;
(ConjNeg (N,h)) . b = (h ") . (N . (h . b)) by CNDef;
hence (ConjNeg (N,h)) . a >= (ConjNeg (N,h)) . b by Rosnie, B1, B2; :: thesis: verum

end;

hence ( ConjNeg (N,h) is satisfying_(N1) & ConjNeg (N,h) is satisfying_(N2) ) by A0, A1, NonInc; :: thesis: verum