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

proof

assume A6: D3 . (len D3) <> upper_bound A ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( D3 . (len D3) > upper_bound A or D3 . (len D3) < upper_bound A ) by A6, XXREAL_0:1;

suppose A7: D3 . (len D3) > upper_bound A ; :: thesis: contradiction

len D3 in Seg (len D3) by FINSEQ_1:3;
then len D3 in dom D3 by FINSEQ_1:def 3;
then D3 . (len D3) in rng D3 by FUNCT_1:def 3;
then D3 . (len D3) in A by A5;
then D3 . (len D3) in [.(lower_bound A),(upper_bound A).] by Th2;
then D3 . (len D3) in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def 1;
then ex a being Real st
( a = D3 . (len D3) & lower_bound A <= a & a <= upper_bound A ) ;
hence contradiction by A7; :: thesis: verum

end;

suppose A8: D3 . (len D3) < upper_bound A ; :: thesis: contradiction

A9: rng D1 c= rng (D1 ^ D2) by FINSEQ_1:29;
len D1 in Seg (len D1) by FINSEQ_1:3;
then A10: len D1 in dom D1 by FINSEQ_1:def 3;
len D3 in Seg (len D3) by FINSEQ_1:3;
then A11: len D3 in dom D3 by FINSEQ_1:def 3;
D1 . (len D1) = upper_bound A by Def1;
then upper_bound A in rng D1 by A10, FUNCT_1:def 3;
then consider k being Nat such that
A12: k in dom D3 and
A13: D3 . k = upper_bound A by A1, A9, FINSEQ_2:10;
k in Seg (len D3) by A12, FINSEQ_1:def 3;
then k <= len D3 by FINSEQ_1:1;
hence contradiction by A8, A11, A12, A13, SEQ_4:137; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then reconsider D3 = D3 as Division of A by A5, Def1;
len D2 = card (rng D2) by FINSEQ_4:62;
then A14: len D2 <= len D3 by A2, FINSEQ_1:30, NAT_1:43;
take D3 ; :: thesis: ( D1 <= D3 & D2 <= D3 )
A15: rng D1 c= rng (D1 ^ D2) by FINSEQ_1:29;
A16: rng D2 c= rng (D1 ^ D2) by FINSEQ_1:30;
len D1 = card (rng D1) by FINSEQ_4:62;
then len D1 <= len D3 by A2, FINSEQ_1:29, NAT_1:43;
hence ( D1 <= D3 & D2 <= D3 ) by A1, A15, A16, A14; :: thesis: verum