theorem :: XXREAL_1:210

for p being ExtReal holds ].p,-infty.[ = {}