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 ) ;
g in REAL by XREAL_0:def 1;
then r in REAL by A4, XXREAL_0:46;
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