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