let X be non empty real-bounded interval Subset of REAL; ( 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 )
; X = ].(lower_bound X),(upper_bound X).[
hence
X c= ].(lower_bound X),(upper_bound X).[
by Th18; XBOOLE_0:def 10 ].(lower_bound X),(upper_bound X).[ c= X
let x be object ; TARSKI:def 3 ( not x in ].(lower_bound X),(upper_bound X).[ or x in X )
assume A1:
x in ].(lower_bound X),(upper_bound X).[
; 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:14;
then consider s being Real such that
A2:
( s in X & s < (lower_bound X) + (x - (lower_bound X)) )
by SEQ_4:def 2;
x < upper_bound X
by A1, XXREAL_1:4;
then
x - x < (upper_bound X) - x
by XREAL_1:14;
then consider r being Real such that
A3:
( r in X & (upper_bound X) - ((upper_bound X) - x) < r )
by SEQ_4:def 1;
( [.s,r.] c= X & x in [.s,r.] )
by A2, A3, XXREAL_1:1, XXREAL_2:def 12;
hence
x in X
; verum