let I be non empty closed_interval Subset of REAL; :: thesis: for r being Real st I = {r} holds
for D being Division of I holds D = <*r*>
let r be Real; :: thesis: ( I = {r} implies for D being Division of I holds D = <*r*> )
assume A1: I = {r} ; :: thesis: for D being Division of I holds D = <*r*>
A2: I = [.r,r.] by A1, XXREAL_1:17;
let D be Division of I; :: thesis: D = <*r*>
len D = 1
proof
assume 1 <> len D ; :: thesis: contradiction
then 2 <= len D by NAT_1:23;
then ( 1 <= len D & 1 <= 2 & 2 <= len D ) by XXREAL_0:2;
then A3: ( 1 in dom D & 2 in dom D ) by FINSEQ_3:25;
then ( D . 1 in I & D . 2 in I ) by INTEGRA1:6;
then ( D . 1 = r & D . 2 = r ) by A1, TARSKI:def 1;
hence contradiction by A3, VALUED_0:def 13; :: thesis: verum
end;
hence D = <*r*> by A2, COUSIN:64; :: thesis: verum