:: deftheorem Reichen defines Reichenbach_implication FUZIMPL1:def 17 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Reichenbach_implication iff for x, y being Element of [.0,1.] holds b₁ . (x,y) = (1 - x) + (x * y) );