let X be bounded Subset of REAL ; :: thesis: ( not lower_bound X in X implies X c= ].(lower_bound X),(upper_bound X).] )
assume A1: not lower_bound X in X ; :: thesis: X c= ].(lower_bound X),(upper_bound X).]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in ].(lower_bound X),(upper_bound X).] )
assume A2: x in X ; :: thesis: x in ].(lower_bound X),(upper_bound X).]
then reconsider x = x as Real ;
A3: x <= upper_bound X by A2, SEQ_4:def 4;
lower_bound X <= x by A2, SEQ_4:def 5;
then lower_bound X < x by A1, A2, XXREAL_0:1;
hence x in ].(lower_bound X),(upper_bound X).] by A3, XXREAL_1:2; :: thesis: verum