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 )
len D1 in Seg (len D1) by FINSEQ_1:5;
then A1: len D1 in dom D1 by FINSEQ_1:def 3;
assume A2: D1 <= D2 ; :: thesis: indx D2,D1,(len D1) = len D2
then D1 . (len D1) = D2 . (indx D2,D1,(len D1)) by A1, Def21;
then A3: D2 . (indx D2,D1,(len D1)) = upper_bound A by Def2;
len D2 in Seg (len D2) by FINSEQ_1:5;
then A4: len D2 in dom D2 by FINSEQ_1:def 3;
assume A5: indx D2,D1,(len D1) <> len D2 ; :: thesis: contradiction
A6: indx D2,D1,(len D1) in dom D2 by A2, A1, Def21;
then indx D2,D1,(len D1) in Seg (len D2) by FINSEQ_1:def 3;
then indx D2,D1,(len D1) <= len D2 by FINSEQ_1:3;
then indx D2,D1,(len D1) < len D2 by A5, XXREAL_0:1;
then D2 . (indx D2,D1,(len D1)) < D2 . (len D2) by A4, A6, SEQM_3:def 1;
hence contradiction by A3, Def2; :: thesis: verum