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 ) } )
A2: ].g,s.] c= { r where r is Real : ( g < r & r <= s ) }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in ].g,s.] or e in { r where r is Real : ( g < r & r <= s ) } )
assume e in ].g,s.] ; :: thesis: e in { r where r is Real : ( g < r & r <= s ) }
then consider r being Element of ExtREAL such that
A3: e = r and
A4: ( g < r & r <= s ) ;
s in REAL by XREAL_0:def 1;
then r in REAL by A4, XXREAL_0:47;
hence e in { r where r is Real : ( g < r & r <= s ) } by A3, A4; :: thesis: verum
end;
{ r where r is Real : ( g < r & r <= s ) } c= ].g,s.]
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { r where r is Real : ( g < r & r <= s ) } or e in ].g,s.] )
assume e in { r where r is Real : ( g < r & r <= s ) } ; :: thesis: e in ].g,s.]
then consider r being Real such that
A5: ( e = r & g < r & r <= s ) ;
r in REAL by XREAL_0:def 1;
hence e in ].g,s.] by A5, NUMBERS:31; :: thesis: verum
end;
hence ( X = ].g,s.] iff X = { r where r is Real : ( g < r & r <= s ) } ) by A2; :: thesis: verum