let a, b be Real; :: thesis: ( a <> b implies Cl ].a,b.] = [.a,b.] )
A1: Cl ].a,b.] c= [.a,b.] by MEASURE6:57, XXREAL_1:23;
A2: Cl ].a,b.[ c= Cl ].a,b.] by MEASURE6:62, XXREAL_1:21;
assume a <> b ; :: thesis: Cl ].a,b.] = [.a,b.]
then [.a,b.] c= Cl ].a,b.] by A2, JORDAN5A:26;
hence Cl ].a,b.] = [.a,b.] by A1, XBOOLE_0:def 10; :: thesis: verum