theorem HamCoIn01: :: FUZNORM1:14

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