:: deftheorem Weber defines Weber_implication FUZIMPL1:def 22 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Weber_implication iff for x, y being Element of [.0,1.] holds
( ( x < 1 implies b₁ . (x,y) = 1 ) & ( x = 1 implies b₁ . (x,y) = y ) ) );