theorem LBProp: :: FUZIMPL1:7

for fi being Fuzzy_Implication
for y being Element of [.0,1.] holds fi . (0,y) = 1