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 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 ) ;
( g in REAL & s in REAL ) by XREAL_0:def 1;
then r in REAL by A4, XXREAL_0:45;
hence x 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 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
A5: ( x = r & g <= r & r <= s ) ;
r in REAL by XREAL_0:def 1;
hence x 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