let X be real-bounded Subset of REAL; :: thesis: ( not upper_bound X in X implies X c= [.(lower_bound X),(upper_bound X).[ )
assume A1: not upper_bound X in X ; :: thesis: X c= [.(lower_bound X),(upper_bound X).[
let x be object ; :: 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 ;
x <= upper_bound X by A2, SEQ_4:def 1;
then A3: x < upper_bound X by A1, A2, XXREAL_0:1;
lower_bound X <= x by A2, SEQ_4:def 2;
hence x in [.(lower_bound X),(upper_bound X).[ by A3, XXREAL_1:3; :: thesis: verum