let X be bounded connected 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, JCT_MISC:def 1; :: thesis: verum