set f = NegationD2 ;
( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
hence NegationD2 is satisfying_(N1) by D2Def; :: thesis: NegationD2 is satisfying_(N2)
for x, y being Element of [.0,1.] st x <= y holds
NegationD2 . x >= NegationD2 . y

proof

let x, y be Element of [.0,1.]; :: thesis: ( x <= y implies NegationD2 . x >= NegationD2 . y )
assume B2: x <= y ; :: thesis: NegationD2 . x >= NegationD2 . y

per cases ( y = 1 or y <> 1 ) ;

suppose y = 1 ; :: thesis: NegationD2 . x >= NegationD2 . y

then NegationD2 . y = 0 by D2Def;
hence NegationD2 . x >= NegationD2 . y by XXREAL_1:1; :: thesis: verum

end;

suppose B1: y <> 1 ; :: thesis: NegationD2 . x >= NegationD2 . y

then B3: NegationD2 . y = 1 by D2Def;
y <= 1 by XXREAL_1:1;
then y < 1 by B1, XXREAL_0:1;
hence NegationD2 . x >= NegationD2 . y by B3, D2Def, B2; :: thesis: verum

end;

end;

end;

hence NegationD2 is satisfying_(N2) by NonInc; :: thesis: verum