:: deftheorem defines less_pred NOMIN_4:def 11 :
for x, y being object holds
( x less_pred y iff ex x1, y1 being ExtReal st
( x1 = x & y1 = y & x1 < y1 ) );