theorem Th10: :: NOMIN_4:10

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