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 A1: ex r being Element of ExtREAL st
( x = r & g <= r & r <= s ) ;
( g in REAL & s in REAL ) by XREAL_0:def 1;
hence x in REAL by A1, XXREAL_0:45; :: thesis: verum

end;

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