theorem OpIn01: :: FUZNORM1:7

for a being Element of [.0,1.] holds 1 - a in [.0,1.]