let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st len D1 = 1 holds
D1 <= D2
let D1, D2 be Division of A; :: thesis: ( len D1 = 1 implies D1 <= D2 )
A1: D2 . (len D2) = upper_bound A by Def1;
assume A2: len D1 = 1 ; :: thesis: D1 <= D2
then D1 . 1 = upper_bound A by Def1;
then D1 = <*(upper_bound A)*> by A2, FINSEQ_1:40;
then A3: rng D1 = {(upper_bound A)} by FINSEQ_1:38;
A4: len D2 in Seg (len D2) by FINSEQ_1:3;
hence len D1 <= len D2 by A2, FINSEQ_1:1; :: according to INTEGRA1:def 18 :: thesis: rng D1 c= rng D2
len D2 in dom D2 by A4, FINSEQ_1:def 3;
then upper_bound A in rng D2 by A1, FUNCT_1:def 3;
then rng D1 is Subset of (rng D2) by A3, SUBSET_1:41;
hence rng D1 c= rng D2 ; :: thesis: verum