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 ) ;
g in REAL by XREAL_0:def 1;
hence e in REAL by A1, XXREAL_0:46; :: thesis: verum
end;
hence [.g,s.[ is Subset of REAL by TARSKI:def 3; :: thesis: verum