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