set Y = { r where r is Real : ( g < r & r < s ) } ;
let X be Subset of REAL; :: thesis: ( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } )
A1: { r where r is Real : ( g < r & r < s ) } c= ].g,s.[

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { r where r is Real : ( g < r & r < s ) } or x in ].g,s.[ )
assume x in { r where r is Real : ( g < r & r < s ) } ; :: thesis: x in ].g,s.[
then consider r being Real such that
A2: ( x = r & g < r & r < s ) ;
r in REAL by XREAL_0:def 1;
hence x in ].g,s.[ by A2, NUMBERS:31; :: thesis: verum

end;

].g,s.[ c= { r where r is Real : ( g < r & r < s ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].g,s.[ or x in { r where r is Real : ( g < r & r < s ) } )
assume x in ].g,s.[ ; :: thesis: x in { r where r is Real : ( g < r & r < s ) }
then consider r being Element of ExtREAL such that
A3: x = r and
A4: ( g < r & r < s ) ;
r in REAL by A4, XXREAL_0:48;
hence x in { r where r is Real : ( g < r & r < s ) } by A3, A4; :: thesis: verum

end;

hence ( X = ].g,s.[ iff X = { r where r is Real : ( g < r & r < s ) } ) by A1; :: thesis: verum