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