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