let f be BinOp of [.0,1.]; :: thesis: ( f is with_properties_of_fuzzy_implication implies f is with_properties_of_classical_implication )

assume A1: f is with_properties_of_fuzzy_implication ; :: thesis: f is with_properties_of_classical_implication

f . (0,1) = 1

hence f is with_properties_of_classical_implication by A1; :: thesis: verum

assume A1: f is with_properties_of_fuzzy_implication ; :: thesis: f is with_properties_of_classical_implication

f . (0,1) = 1

proof

then
f is 01-dominant
;
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; :: thesis: verum

end;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; :: thesis: verum

hence f is with_properties_of_classical_implication by A1; :: thesis: verum