let X be interval Subset of REAL; :: thesis: ( X is bounded_below & not X is bounded_above & lower_bound X in X implies X = right_closed_halfline (lower_bound X) )
assume that
A1: X is bounded_below and
A2: not X is bounded_above and
A3: lower_bound X in X ; :: thesis: X = right_closed_halfline (lower_bound X)
thus X c= right_closed_halfline (lower_bound X) by A1, Th24; :: according to XBOOLE_0:def 10 :: thesis: right_closed_halfline (lower_bound X) c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in right_closed_halfline (lower_bound X) or x in X )
assume A4: x in right_closed_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 and
A6: x < r by XXREAL_2:def 1;
reconsider r = r as Real by A5;
lower_bound X <= x by A4, XXREAL_1:236;
then A7: x in [.(lower_bound X),r.] by A6, XXREAL_1:1;
[.(lower_bound X),r.] c= X by A3, A5, XXREAL_2:def 12;
hence x in X by A7; :: thesis: verum