let X be real-bounded interval 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, Th16; :: according to XBOOLE_0:def 10 :: thesis: [.(lower_bound X),(upper_bound X).[ c= X
let x be object ; :: 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 ;
x < upper_bound X by A3, XXREAL_1:3;
then x - x < (upper_bound X) - x by XREAL_1:14;
then consider r being Real such that
A4: r in X and
A5: (upper_bound X) - ((upper_bound X) - x) < r by A1, SEQ_4:def 1;
lower_bound X <= x by A3, XXREAL_1:3;
then A6: x in [.(lower_bound X),r.] by A5, XXREAL_1:1;
[.(lower_bound X),r.] c= X by A1, A4, XXREAL_2:def 12;
hence x in X by A6; :: thesis: verum