let A be 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) & len D3 = card (rng (D1 ^ D2)) & D3 is increasing ) by GOBOARD2:21;
reconsider D3 = D3 as non empty increasing FinSequence of REAL by A1;
A2: rng D1 c= A by Def2;
rng D2 c= A by Def2;
then (rng D1) \/ (rng D2) c= A by A2, XBOOLE_1:8;
then A3: rng D3 c= A by A1, FINSEQ_1:44;
D3 . (len D3) = upper_bound A

proof

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

now

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

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

len D3 in Seg (len D3) by FINSEQ_1:5;
then len D3 in dom D3 by FINSEQ_1:def 3;
then D3 . (len D3) in rng D3 by FUNCT_1:def 5;
then D3 . (len D3) in A by A3;
then D3 . (len D3) in [.(lower_bound A),(upper_bound A).] by Th5;
then D3 . (len D3) in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def 1;
then consider a being Real such that
A6: ( a = D3 . (len D3) & lower_bound A <= a & a <= upper_bound A ) ;
thus contradiction by A5, A6; :: thesis: verum

end;

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

len D3 in Seg (len D3) by FINSEQ_1:5;
then A8: len D3 in dom D3 by FINSEQ_1:def 3;
len D1 in Seg (len D1) by FINSEQ_1:5;
then A9: len D1 in dom D1 by FINSEQ_1:def 3;
A10: rng D1 c= rng (D1 ^ D2) by FINSEQ_1:42;
D1 . (len D1) = upper_bound A by Def2;
then upper_bound A in rng D1 by A9, FUNCT_1:def 5;
then consider k being Nat such that
A11: ( k in dom D3 & D3 . k = upper_bound A ) by A1, A10, FINSEQ_2:11;
k in Seg (len D3) by A11, FINSEQ_1:def 3;
then k <= len D3 by FINSEQ_1:3;
hence contradiction by A7, A8, A11, GOBOARD2:18; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then reconsider D3 = D3 as Division of A by A3, Def2;
D1 is one-to-one by JORDAN7:17;
then A12: len D1 = card (rng D1) by FINSEQ_4:77;
D2 is one-to-one by JORDAN7:17;
then A13: len D2 = card (rng D2) by FINSEQ_4:77;
A14: rng D1 c= rng (D1 ^ D2) by FINSEQ_1:42;
A15: len D1 <= len D3 by A1, A12, FINSEQ_1:42, NAT_1:44;
A16: rng D2 c= rng (D1 ^ D2) by FINSEQ_1:43;
A17: len D2 <= len D3 by A1, A13, FINSEQ_1:43, NAT_1:44;
take D3 ; :: thesis: ( D1 <= D3 & D2 <= D3 )
thus ( D1 <= D3 & D2 <= D3 ) by A1, A14, A15, A16, A17, Def20; :: thesis: verum