let X be real-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).]
reconsider X1 = X as non empty real-bounded interval Subset of REAL by A1;
X1 c= [.(lower_bound X1),(upper_bound X1).] by XXREAL_2:69;
hence X c= [.(lower_bound X),(upper_bound X).] ; :: 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