let s be ext-real number ; :: 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 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 B1: ( -infty < x & x < s ) by Th4;
then x in REAL by XXREAL_0:48;
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, Th4; :: thesis: verum