let a, b be real number ; :: thesis: ( a <> b implies Cl ].a,b.] = [.a,b.] )
A1: Cl ].a,b.] c= [.a,b.] by MEASURE6:93, XXREAL_1:23;
A2: Cl ].a,b.[ c= Cl ].a,b.] by MEASURE6:98, XXREAL_1:21;
assume a <> b ; :: thesis: Cl ].a,b.] = [.a,b.]
then [.a,b.] c= Cl ].a,b.] by A2, TOPREAL6:82;
hence Cl ].a,b.] = [.a,b.] by A1, XBOOLE_0:def 10; :: thesis: verum