let A, B be closed-interval Subset of REAL ; :: thesis: ( A c= B implies vol A <= vol B )
assume A1: A c= B ; :: thesis: vol A <= vol B
A3: ( lower_bound A >= lower_bound B & upper_bound A <= upper_bound B ) by A1, SEQ_4:64, SEQ_4:65;
vol A = (upper_bound A) - (lower_bound A) by INTEGRA1:def 6;
then upper_bound B >= (vol A) + (lower_bound A) by A1, SEQ_4:65;
then (upper_bound B) - (vol A) >= lower_bound A by XREAL_1:21;
then (upper_bound B) - (vol A) >= lower_bound B by A3, XXREAL_0:2;
then (upper_bound B) - (lower_bound B) >= vol A by XREAL_1:13;
hence vol A <= vol B by INTEGRA1:def 6; :: thesis: verum