let A be non empty closed_interval Subset of REAL; :: thesis:
let D1, D2 be Division of A; :: thesis:
consider D being FinSequence of REAL such that
A1: rng D = rng (D1 ^ D2) and
A2: len D = card (rng (D1 ^ D2)) and
A3: D is increasing by SEQ_4:140;
reconsider D = D as increasing FinSequence of REAL by A3;
reconsider D = D as non empty increasing FinSequence of REAL by A1;
A4: rng D2 c= A by INTEGRA1:def 2;
A5: rng (D1 ^ D2) = (rng D1) \/ (rng D2) by FINSEQ_1:31;
then A6: rng D1 c= rng (D1 ^ D2) by XBOOLE_1:7;
rng D1 c= A by INTEGRA1:def 2;
then A7: rng D c= A by A1, A5, A4, XBOOLE_1:8;
D . (len D) = upper_bound A

len D1 in dom D1 by FINSEQ_5:6;
then D1 . (len D1) in rng D1 by FUNCT_1:def 3;
then consider k being Element of NAT such that
A8: k in dom D and
A9: D1 . (len D1) = D . k by A1, A6, PARTFUN1:3;
assume A10: D . (len D) <> upper_bound A ; :: thesis:
A11: len D in dom D by FINSEQ_5:6;
then D . (len D) in rng D by FUNCT_1:def 3;
then D . (len D) <= upper_bound A by A7, INTEGRA2:1;
then A12: D . (len D) < upper_bound A by A10, XXREAL_0:1;
D1 . (len D1) = upper_bound A by INTEGRA1:def 2;
then k > len D by A11, A12, A8, A9, SEQ_4:137;
hence contradiction by A8, FINSEQ_3:25; :: thesis:

end;

then reconsider D = D as Division of A by A7, INTEGRA1:def 2;
take D ; :: thesis:
card (rng D1) <= len D by A2, A5, NAT_1:43, XBOOLE_1:7;
then len D1 <= len D by FINSEQ_4:62;
hence D1 <= D by A1, A6, INTEGRA1:def 18; :: thesis:
A13: rng D2 c= rng (D1 ^ D2) by A5, XBOOLE_1:7;
card (rng D2) <= len D by A2, A5, NAT_1:43, XBOOLE_1:7;
then len D2 <= len D by FINSEQ_4:62;
hence D2 <= D by A1, A13, INTEGRA1:def 18; :: thesis:
thus rng D = (rng D1) \/ (rng D2) by A1, FINSEQ_1:31; :: thesis: