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