theorem HamIn01: :: FUZNORM1:9

for a, b being Element of [.0,1.] holds (a * b) / ((a + b) - (a * b)) in [.0,1.]