theorem :: XXREAL_1:230

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