for x, y being ExtReal holds
( x less_pred y or y less_pred x or x = y )