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 A1: x in ].-infty,s.[ ; :: thesis: x in { g where g is Real : g < s }
then A2: -infty < x by Th4;
A3: x < s by A1, Th4;
then x in REAL by A2, XXREAL_0:48;
hence x in { g where g is Real : g < s } by A3; :: 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
A4: x = g and
A5: g < s ;
-infty < g by XXREAL_0:12;
hence x in ].-infty,s.[ by A4, A5, Th4; :: thesis: verum