theorem :: XXREAL_1:231

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