let s be Real; :: thesis: ].-infty,s.] = { g where g is Real : g <= s }
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; :: 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 A1: x <= s by Th2;
thus x in { g where g is Real : g <= s } by A1; :: thesis: verum

end;

let x be object ; :: 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 and
A3: g <= s ;
g in REAL by XREAL_0:def 1;
then -infty < g by XXREAL_0:12;
hence x in ].-infty,s.] by A2, A3, Th2; :: thesis: verum