for t being commutative monotonic with-0-identity BinOp of [.0,1.]
for a being Element of [.0,1.] holds t . (a,1) = 1