let a be Real; :: thesis: {a} is thin of B-Meas
set A = [.a,a.];
reconsider E = {a} as Subset of REAL ;
A1: [.a,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: E c= [.a,a.] by XXREAL_1:17;
reconsider a1 = a as R_eal by XXREAL_0:def 1;
B-Meas . [.a,a.] = diameter [.a,a.] by Th72
.= a1 - a1 by MEASURE5:6
.= a - a by Lm9
.= 0 ;
hence {a} is thin of B-Meas by A3, A2, A1, A4, MEASURE3:def 2; :: thesis: verum