let X be non empty bounded interval Subset of REAL; :: thesis: ( not lower_bound X in X & not upper_bound X in X implies X = ].(lower_bound X),(upper_bound X).[ )
assume ( not lower_bound X in X & not upper_bound X in X ) ; :: thesis: X = ].(lower_bound X),(upper_bound X).[
hence X c= ].(lower_bound X),(upper_bound X).[ by Th30; :: 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 A1: x in ].(lower_bound X),(upper_bound X).[ ; :: thesis: x in X
then reconsider x = x as Real ;
lower_bound X < x by A1, XXREAL_1:4;
then (lower_bound X) - (lower_bound X) < x - (lower_bound X) by XREAL_1:16;
then consider s being real number such that
A2: ( s in X & s < (lower_bound X) + (x - (lower_bound X)) ) by SEQ_4:def 5;
x < upper_bound X by A1, XXREAL_1:4;
then x - x < (upper_bound X) - x by XREAL_1:16;
then consider r being real number such that
A3: ( r in X & (upper_bound X) - ((upper_bound X) - x) < r ) by SEQ_4:def 4;
( [.s,r.] c= X & x in [.s,r.] ) by A2, A3, XXREAL_2:def 12, XXREAL_1:1;
hence x in X ; :: thesis: verum