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

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

end;

then f is 01-dominant ;
hence f is with_properties_of_classical_implication by A1; :: thesis: verum