theorem Th5: :: MESFUN14:5

for a, b being Real st a <= b holds
( B-Meas . [.a,b.] = b - a & B-Meas . [.a,b.[ = b - a & B-Meas . ].a,b.] = b - a & B-Meas . ].a,b.[ = b - a & L-Meas . [.a,b.] = b - a & L-Meas . [.a,b.[ = b - a & L-Meas . ].a,b.] = b - a & L-Meas . ].a,b.[ = b - a )