let X be Subset of REAL; :: thesis: ( X is bounded_below & not lower_bound X in X implies X c= right_open_halfline (lower_bound X) )
assume that
A1: X is bounded_below and
A2: not lower_bound X in X ; :: thesis: X c= right_open_halfline (lower_bound X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in right_open_halfline (lower_bound X) )
assume A3: x in X ; :: thesis: x in right_open_halfline (lower_bound X)
then reconsider x = x as Real ;
lower_bound X <= x by A1, A3, SEQ_4:def 2;
then lower_bound X < x by A2, A3, XXREAL_0:1;
hence x in right_open_halfline (lower_bound X) by XXREAL_1:235; :: thesis: verum