let X be connected 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 set ; :: 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 ;
consider r being real number such that
A3: r in X and
A4: r > x by A1, SEQ_4:def 1;
consider s being real number such that
A5: s in X and
A6: s < x by A2, SEQ_4:def 2;
A7: [.s,r.] c= X by A3, A5, JCT_MISC:def 1;
x in [.s,r.] by A4, A6, XXREAL_1:1;
hence x in X by A7; :: thesis: verum