let X be bounded interval Subset of REAL ; :: thesis: ( lower_bound X in X & upper_bound X in X implies X = [.(lower_bound X),(upper_bound X).] )
assume A1: ( lower_bound X in X & upper_bound X in X ) ; :: thesis: X = [.(lower_bound X),(upper_bound X).]
thus X c= [.(lower_bound X),(upper_bound X).] by TOPREAL6:24; :: according to XBOOLE_0:def 10 :: thesis: [.(lower_bound X),(upper_bound X).] c= X
thus [.(lower_bound X),(upper_bound X).] c= X by A1, XXREAL_2:def 12; :: thesis: verum