now :: thesis: for e being object st e in ].g,s.] holds
e in REAL

let e be object ; :: thesis: ( e in ].g,s.] implies e in REAL )
assume e in ].g,s.] ; :: thesis: e in REAL
then A1: ex r being Element of ExtREAL st
( e = r & g < r & r <= s ) ;
s in REAL by XREAL_0:def 1;
hence e in REAL by A1, XXREAL_0:47; :: thesis: verum

end;

hence ].g,s.] is Subset of REAL by TARSKI:def 3; :: thesis: verum