let f be BinOp of [.0,1.]; ( f is with_properties_of_fuzzy_implication implies f is with_properties_of_classical_implication )
assume A1:
f is with_properties_of_fuzzy_implication
; f is with_properties_of_classical_implication
f . (0,1) = 1
proof
B1:
(
0 in [.0,1.] & 1
in [.0,1.] )
by XXREAL_1:1;
B2:
(
f is
increasing_on_2nd &
f is
00-dominant )
by A1;
then B3:
f . (
0,
0)
<= f . (
0,1)
by B1;
reconsider e0 =
0 ,
e1 = 1 as
Element of
[.0,1.] by XXREAL_1:1;
f . (
e0,
e1)
<= 1
by XXREAL_1:1;
hence
f . (
0,1)
= 1
by B2, B3, XXREAL_0:1;
verum
end;
then
f is 01-dominant
;
hence
f is with_properties_of_classical_implication
by A1; verum