for k being ExtReal holds ExtREAL \ [.-infty,k.] = ].k,+infty.]