let X be non empty connected Subset of REAL ; :: thesis: ( not X is bounded_below & X is bounded_above & not upper_bound X in X implies X = left_open_halfline (upper_bound X) )
assume that
A1: not X is bounded_below and
A2: X is bounded_above and
A3: not upper_bound X in X ; :: thesis: X = left_open_halfline (upper_bound X)
thus X c= left_open_halfline (upper_bound X) by A2, A3, Th34; :: according to XBOOLE_0:def 10 :: thesis: left_open_halfline (upper_bound X) c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in left_open_halfline (upper_bound X) or x in X )
assume A4: x in left_open_halfline (upper_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 A1, SEQ_4:def 2;
x < upper_bound X by A4, XXREAL_1:233;
then x - x < (upper_bound X) - x by XREAL_1:16;
then consider s being real number such that
A7: s in X and
A8: (upper_bound X) - ((upper_bound X) - x) < s by A2, SEQ_4:def 4;
A9: [.r,s.] c= X by A5, A7, JCT_MISC:def 1;
x in [.r,s.] by A6, A8, XXREAL_1:1;
hence x in X by A9; :: thesis: verum