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

proof

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

per cases ;

suppose A1: x = 0 ; :: thesis:

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

end;

suppose x <> 0 ; :: thesis:

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

end;

end;

end;

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

per cases ;

suppose A1: x = 1 ; :: thesis:

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

end;

suppose x <> 1 ; :: thesis:

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

end;

end;