let X be non empty interval 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, Th26; :: according to XBOOLE_0:def 10 :: thesis: right_open_halfline (lower_bound X) c= X
let x be object ; :: 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 ;
x is not UpperBound of X by A2;
then consider r being ExtReal such that
A5: ( r in X & x < r ) by XXREAL_2: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:14;
then consider s being Real such that
A6: ( s in X & s < (lower_bound X) + (x - (lower_bound X)) ) by A1, SEQ_4:def 2;
reconsider r = r as Real by A5;
( [.s,r.] c= X & x in [.s,r.] ) by A5, A6, XXREAL_1:1, XXREAL_2:def 12;
hence x in X ; :: thesis: verum