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