:: deftheorem Def1 defines <= XXREAL_3:def 1 :
for x, y being ExtReal holds
( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st
( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) );