let s be real number ; :: thesis: ].-infty ,s.] = { g where g is Real : g <= s }
F: s in REAL by XREAL_0:def 1;
thus ].-infty ,s.] c= { g where g is Real : g <= s } :: according to XBOOLE_0:def 10 :: thesis: { g where g is Real : g <= s } c= ].-infty ,s.]

proof

let x be real number ; :: according to MEMBERED:def 9 :: thesis: ( not x in ].-infty ,s.] or x in { g where g is Real : g <= s } )
assume x in ].-infty ,s.] ; :: thesis: x in { g where g is Real : g <= s }
then x in ].-infty ,s.] ;
then B1: ( -infty < x & x <= s ) by Th2;
then x in REAL by F, XXREAL_0:47;
hence x in { g where g is Real : g <= s } by B1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { g where g is Real : g <= s } or x in ].-infty ,s.] )
assume x in { g where g is Real : g <= s } ; :: thesis: x in ].-infty ,s.]
then consider g being Real such that
A2: ( x = g & g <= s ) ;
-infty < g by XXREAL_0:12;
hence x in ].-infty ,s.] by A2, Th2; :: thesis: verum