:: deftheorem HamCoDef defines Hamacher_conorm FUZNORM1:def 17 :
for b1 being BinOp of [.0,1.] holds
( b1 = Hamacher_conorm iff for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b1 . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b1 . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) );