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

proof

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

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: NegationD1 . x >= NegationD1 . y

then NegationD1 . x = 1 by D1Def;
hence NegationD1 . x >= NegationD1 . y by XXREAL_1:1; :: thesis: verum

end;

suppose B1: x <> 0 ; :: thesis: NegationD1 . x >= NegationD1 . y

then B3: NegationD1 . x = 0 by D1Def;
x > 0 by B1, XXREAL_1:1;
hence NegationD1 . x >= NegationD1 . y by B3, D1Def, B2; :: thesis: verum

end;

end;

end;

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