let A, B be non empty closed_interval Subset of REAL; :: thesis: ( A c= B implies vol A <= vol B )
assume A1: A c= B ; :: thesis: vol A <= vol B
vol A = (upper_bound A) - (lower_bound A) by INTEGRA1:def 5;
then upper_bound B >= (vol A) + (lower_bound A) by A1, SEQ_4:48;
then A2: (upper_bound B) - (vol A) >= lower_bound A by XREAL_1:19;
lower_bound A >= lower_bound B by A1, SEQ_4:47;
then (upper_bound B) - (vol A) >= lower_bound B by A2, XXREAL_0:2;
then (upper_bound B) - (lower_bound B) >= vol A by XREAL_1:11;
hence vol A <= vol B by INTEGRA1:def 5; :: thesis: verum