let X be bounded connected Subset of REAL ; :: thesis: ( lower_bound X in X & not upper_bound X in X implies X = [.(lower_bound X),(upper_bound X).[ )
assume that
A1: lower_bound X in X and
A2: not upper_bound X in X ; :: thesis: X = [.(lower_bound X),(upper_bound X).[
thus X c= [.(lower_bound X),(upper_bound X).[ by A2, Th28; :: according to XBOOLE_0:def 10 :: thesis: [.(lower_bound X),(upper_bound X).[ c= X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.(lower_bound X),(upper_bound X).[ or x in X )
assume A3: x in [.(lower_bound X),(upper_bound X).[ ; :: thesis: x in X
then reconsider x = x as Real ;
A4: lower_bound X <= x by A3, XXREAL_1:3;
x < upper_bound X by A3, XXREAL_1:3;
then x - x < (upper_bound X) - x by XREAL_1:16;
then consider r being real number such that
A5: r in X and
A6: (upper_bound X) - ((upper_bound X) - x) < r by A1, SEQ_4:def 4;
A7: [.(lower_bound X),r.] c= X by A1, A5, JCT_MISC:def 1;
x in [.(lower_bound X),r.] by A4, A6, XXREAL_1:1;
hence x in X by A7; :: thesis: verum