let A be Interval; :: thesis: B-Meas . A = diameter A
A1: A in Family_of_Intervals by MEASUR10:def 1;
A2: Family_of_Intervals c= Field_generated_by Family_of_Intervals by SRINGS_3:21;
A3: Field_generated_by Family_of_Intervals c= Borel_Sets by PROB_1:def 9, MEASUR10:6;
A4: Field_generated_by Family_of_Intervals c= sigma_Field (C_Meas J-Meas) by MEASURE8:20;
B-Meas . A = (sigma_Meas (C_Meas J-Meas)) . A by A3, A2, A1, FUNCT_1:49
.= (C_Meas J-Meas) . A by A4, A2, A1, MEASURE4:def 3
.= J-Meas . A by A2, A1, MEASURE8:18 ;
hence B-Meas . A = diameter A by Th71; :: thesis: verum