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