let A be non empty closed_interval Subset of REAL; 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; ( D1 <= D2 implies indx (D2,D1,(len D1)) = len D2 )
len D1 in Seg (len D1)
by FINSEQ_1:3;
then A1:
len D1 in dom D1
by FINSEQ_1:def 3;
assume A2:
D1 <= D2
; indx (D2,D1,(len D1)) = len D2
then
D1 . (len D1) = D2 . (indx (D2,D1,(len D1)))
by A1, Def18;
then A3:
D2 . (indx (D2,D1,(len D1))) = upper_bound A
by Def1;
len D2 in Seg (len D2)
by FINSEQ_1:3;
then A4:
len D2 in dom D2
by FINSEQ_1:def 3;
assume A5:
indx (D2,D1,(len D1)) <> len D2
; contradiction
A6:
indx (D2,D1,(len D1)) in dom D2
by A2, A1, Def18;
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:1;
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, Def1; verum