theorem :: XXREAL_1:232

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