let A, B be non empty closed_interval Subset of REAL; :: thesis: ( B c= A implies ( lower_bound A <= lower_bound B & upper_bound B <= upper_bound A ) )
assume B c= A ; :: thesis: ( lower_bound A <= lower_bound B & upper_bound B <= upper_bound A )
then [.(lower_bound B),(upper_bound B).] c= A by INTEGRA1:4;
then A2: [.(lower_bound B),(upper_bound B).] c= [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
lower_bound B <= upper_bound B by SEQ_4:11;
hence ( lower_bound A <= lower_bound B & upper_bound B <= upper_bound A ) by XXREAL_1:50, A2; :: thesis: verum