theorem :: XXREAL_1:233

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