theorem LemmaBound: :: FUZIMPL3:10

for f being bijective increasing UnOp of [.0,1.] holds
( f . 0 = 0 & f . 1 = 1 )