for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.]
for x being Element of [.0,1.] holds x <= (FNegation I) . ((FNegation I) . x)