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:24;
A2: Cl ].a,b.[ c= Cl [.a,b.[ by MEASURE6:62, XXREAL_1:22;
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