let X be real-bounded interval Subset of REAL; :: thesis: ( not lower_bound X in X & upper_bound X in X implies X = ].(lower_bound X),(upper_bound X).] )
assume that
A1: not lower_bound X in X and
A2: upper_bound X in X ; :: thesis: X = ].(lower_bound X),(upper_bound X).]
thus X c= ].(lower_bound X),(upper_bound X).] by A1, Th14; :: 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 ;
lower_bound X < x by A3, XXREAL_1:2;
then (lower_bound X) - (lower_bound X) < x - (lower_bound X) by XREAL_1:14;
then consider r being Real such that
A4: r in X and
A5: r < (lower_bound X) + (x - (lower_bound X)) by A2, SEQ_4:def 2;
x <= upper_bound X by A3, XXREAL_1:2;
then A6: x in [.r,(upper_bound X).] by A5, XXREAL_1:1;
[.r,(upper_bound X).] c= X by A2, A4, XXREAL_2:def 12;
hence x in X by A6; :: thesis: verum