let X be interval Subset of REAL; :: thesis: ( not X is bounded_above & not X is bounded_below implies X = REAL )
assume that
A1: not X is bounded_above and
A2: not X is bounded_below ; :: thesis: X = REAL
thus X c= REAL ; :: according to XBOOLE_0:def 10 :: thesis: REAL c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL or x in X )
assume x in REAL ; :: thesis: x in X
then reconsider x = x as Real ;
x is not UpperBound of X by A1;
then consider r being ExtReal such that
A3: ( r in X & r > x ) by XXREAL_2:def 1;
reconsider r = r as Real by A3;
x is not LowerBound of X by A2;
then consider s being ExtReal such that
A4: ( s in X & s < x ) by XXREAL_2:def 2;
reconsider s = s as Real by A4;
( [.s,r.] c= X & x in [.s,r.] ) by A3, A4, XXREAL_1:1, XXREAL_2:def 12;
hence x in X ; :: thesis: verum