theorem :: XXREAL_1:229

for s being ExtReal holds ].-infty,s.[ = { g where g is Real : g < s }