theorem CoIn01: :: FUZNORM1:16

for f being BinOp of [.0,1.]
for a, b being Real holds 1 - (f . ((1 - a),(1 - b))) in [.0,1.]