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

let x be object ; :: thesis: ( x in ].g,s.[ implies x in REAL )
assume x in ].g,s.[ ; :: thesis: x in REAL
then ex r being Element of ExtREAL st
( x = r & g < r & r < s ) ;
hence x in REAL by XXREAL_0:48; :: thesis: verum

end;

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