theorem :: XXREAL_1:234

for u being ExtReal
for x being Real holds
( x in ].-infty,u.] iff x <= u )