theorem RBProp: :: FUZIMPL1:8
for fi being Fuzzy_Implication
for x being Element of [.0,1.] holds fi . (x,1) = 1