:: deftheorem LukConorm defines BoundedSum_conorm FUZNORM1:def 19 :
for b1 being BinOp of [.0,1.] holds
( b1 = BoundedSum_conorm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = min ((a + b),1) );