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.];
( a <= b implies (ConjNeg (N,h)) . a >= (ConjNeg (N,h)) . b )
assume
a <= b
;
(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;
verum
end;
hence
( ConjNeg (N,h) is satisfying_(N1) & ConjNeg (N,h) is satisfying_(N2) )
by A0, A1, NonInc; verum