let A, B be non empty closed_interval Subset of REAL; :: thesis: ( not B c< A or lower_bound A < lower_bound B or upper_bound B < upper_bound A )
assume B c< A ; :: thesis: ( lower_bound A < lower_bound B or 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 or upper_bound B < upper_bound A ) by A2, XXREAL_1:82; :: thesis: verum