let X be bounded Subset of REAL ; :: thesis: ( not lower_bound X in X & not upper_bound X in X implies X c= ].(lower_bound X),(upper_bound X).[ )
assume that
A1: not lower_bound X in X and
A2: not upper_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 A3: x in X ; :: thesis: x in ].(lower_bound X),(upper_bound X).[
then reconsider x = x as Real ;
( lower_bound X <= x & x <= upper_bound X ) by A3, SEQ_4:def 4, SEQ_4:def 5;
then ( lower_bound X < x & x < upper_bound X ) by A1, A2, A3, XXREAL_0:1;
hence x in ].(lower_bound X),(upper_bound X).[ by XXREAL_1:4; :: thesis: verum