:: deftheorem defines with_properties_of_fuzzy_implication FUZIMPL1:def 7 :
for f being BinOp of [.0,1.] holds
( f is with_properties_of_fuzzy_implication iff ( f is decreasing_on_1st & f is increasing_on_2nd & f is 00-dominant & f is 11-dominant & f is 10-weak ) );