set f = NegationD1 ;
set g = NegationD2 ;
let N be Fuzzy_Negation; :: thesis: ( NegationD1 <= N & N <= NegationD2 )
thus NegationD1 <= N :: thesis: N <= NegationD2

proof

let x be Element of [.0,1.]; :: according to FUZIMPL3:def 19 :: thesis: NegationD1 . x <= N . x

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

suppose A1: x = 0 ; :: thesis: NegationD1 . x <= N . x

then NegationD1 . x = 1 by D1Def;
hence NegationD1 . x <= N . x by A1, N1Def; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: NegationD1 . x <= N . x

then NegationD1 . x = 0 by D1Def;
hence NegationD1 . x <= N . x by XXREAL_1:1; :: thesis: verum

end;

end;

end;

let x be Element of [.0,1.]; :: according to FUZIMPL3:def 19 :: thesis: N . x <= NegationD2 . x

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

suppose A1: x = 1 ; :: thesis: N . x <= NegationD2 . x

then N . x = 0 by N1Def;
hence N . x <= NegationD2 . x by A1, D2Def; :: thesis: verum

end;

suppose x <> 1 ; :: thesis: N . x <= NegationD2 . x

then NegationD2 . x = 1 by D2Def;
hence N . x <= NegationD2 . x by XXREAL_1:1; :: thesis: verum

end;

end;