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