let X be non empty connected Subset of REAL ; :: thesis: ( X is bounded_below & not X is bounded_above & not lower_bound X in X implies X = right_open_halfline (lower_bound X) )
assume that
A1: X is bounded_below and
A2: not X is bounded_above and
A3: not lower_bound X in X ; :: thesis: X = right_open_halfline (lower_bound X)
thus X c= right_open_halfline (lower_bound X) by A1, A3, Th38; :: according to XBOOLE_0:def 10 :: thesis: right_open_halfline (lower_bound X) c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in right_open_halfline (lower_bound X) or x in X )
assume A4: x in right_open_halfline (lower_bound X) ; :: thesis: x in X
then reconsider x = x as Real ;
consider r being real number such that
A5: r in X and
A6: x < r by A2, SEQ_4:def 1;
lower_bound X < x by A4, XXREAL_1:235;
then (lower_bound X) - (lower_bound X) < x - (lower_bound X) by XREAL_1:16;
then consider s being real number such that
A7: s in X and
A8: s < (lower_bound X) + (x - (lower_bound X)) by A1, SEQ_4:def 5;
A9: [.s,r.] c= X by A5, A7, JCT_MISC:def 1;
x in [.s,r.] by A6, A8, XXREAL_1:1;
hence x in X by A9; :: thesis: verum