theorem :: XXREAL_1:236

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