let A be closed-interval Subset of REAL ; :: thesis: for D1, D2 being Division of A st D1 <= D2 holds
indx D2,D1,(len D1) = len D2
let D1, D2 be Division of A; :: thesis: ( D1 <= D2 implies indx D2,D1,(len D1) = len D2 )
assume A1: D1 <= D2 ; :: thesis: indx D2,D1,(len D1) = len D2
assume A2: indx D2,D1,(len D1) <> len D2 ; :: thesis: contradiction
A3: len D1 in dom D1

proof

len D1 in Seg (len D1) by FINSEQ_1:5;
hence len D1 in dom D1 by FINSEQ_1:def 3; :: thesis: verum

end;

then D1 . (len D1) = D2 . (indx D2,D1,(len D1)) by A1, Def21;
then A4: D2 . (indx D2,D1,(len D1)) = upper_bound A by Def2;
A5: len D2 in dom D2

proof

len D2 in Seg (len D2) by FINSEQ_1:5;
hence len D2 in dom D2 by FINSEQ_1:def 3; :: thesis: verum

end;

A6: indx D2,D1,(len D1) in dom D2 by A1, A3, Def21;
indx D2,D1,(len D1) < len D2

proof

indx D2,D1,(len D1) in Seg (len D2) by A6, FINSEQ_1:def 3;
then indx D2,D1,(len D1) <= len D2 by FINSEQ_1:3;
hence indx D2,D1,(len D1) < len D2 by A2, XXREAL_0:1; :: thesis: verum

end;

then D2 . (indx D2,D1,(len D1)) < D2 . (len D2) by A5, A6, SEQM_3:def 1;
hence contradiction by A4, Def2; :: thesis: verum