let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st D1 <= D2 holds
for j being Nat st j in dom D2 holds
ex i being Nat st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )
let D1, D2 be Division of A; :: thesis: ( D1 <= D2 implies for j being Nat st j in dom D2 holds
ex i being Nat st
( i in dom D1 & divset (D2,j) c= divset (D1,i) ) )
assume A1: D1 <= D2 ; :: thesis: for j being Nat st j in dom D2 holds
ex i being Nat st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )
let j be Nat; :: thesis: ( j in dom D2 implies ex i being Nat st
( i in dom D1 & divset (D2,j) c= divset (D1,i) ) )
defpred S₁[ set ] means ( D2 . $1 in rng D1 & D2 . $1 >= D2 . j );
consider X being Subset of (dom D2) such that
A2: for x1 being set holds
( x1 in X iff ( x1 in dom D2 & S₁[x1] ) ) from SUBSET_1:sch 1();
reconsider X = X as Subset of NAT by XBOOLE_1:1;
assume A3: j in dom D2 ; :: thesis: ex i being Nat st
( i in dom D1 & divset (D2,j) c= divset (D1,i) )
ex n being Nat st
( n in dom D2 & D2 . n in rng D1 & D2 . n >= D2 . j )

proof

take len D2 ; :: thesis: ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j )
len D2 in Seg (len D2) by FINSEQ_1:3;
then A4: len D2 in dom D2 by FINSEQ_1:def 3;
len D1 in Seg (len D1) by FINSEQ_1:3;
then A5: len D1 in dom D1 by FINSEQ_1:def 3;
D2 . (len D2) = upper_bound A by INTEGRA1:def 2;
then A6: D1 . (len D1) = D2 . (len D2) by INTEGRA1:def 2;
j in Seg (len D2) by A3, FINSEQ_1:def 3;
then j <= len D2 by FINSEQ_1:1;
hence ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j ) by A3, A5, A6, A4, FUNCT_1:def 3, SEQ_4:137; :: thesis: verum

end;

then reconsider X = X as non empty Subset of NAT by A2;
A7: min X in X by XXREAL_2:def 7;
then A8: D2 . (min X) >= D2 . j by A2;
D2 . (min X) in rng D1 by A2, A7;
then consider i being Element of NAT such that
A9: i in dom D1 and
A10: D2 . (min X) = D1 . i by PARTFUN1:3;
take i ; :: thesis: ( i in dom D1 & divset (D2,j) c= divset (D1,i) )
A11: D1 . i >= D2 . j by A2, A7, A10;
divset (D2,j) c= divset (D1,i)

proof

now :: thesis: divset (D2,j) c= divset (D1,i)

per cases ( i = 1 or i <> 1 ) ;

suppose i = 1 ; :: thesis: divset (D2,j) c= divset (D1,i)

then ( lower_bound (divset (D1,i)) = lower_bound A & upper_bound (divset (D1,i)) = D1 . i ) by A9, INTEGRA1:def 4;
then A12: divset (D1,i) = [.(lower_bound A),(D1 . i).] by INTEGRA1:4;

now :: thesis: divset (D2,j) c= divset (D1,i)

per cases ( j = 1 or j <> 1 ) ;

suppose A13: j = 1 ; :: thesis: divset (D2,j) c= divset (D1,i)

( D1 . i in rng D1 & rng D1 c= A ) by A9, FUNCT_1:def 3, INTEGRA1:def 2;
then A14: D1 . i in A ;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then D1 . i in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A14, RCOMP_1:def 1;
then ex x being Real st
( x = D1 . i & lower_bound A <= x & x <= upper_bound A ) ;
then lower_bound A in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } ;
then A15: lower_bound A in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1;
( D2 . j in rng D2 & rng D2 c= A ) by A3, FUNCT_1:def 3, INTEGRA1:def 2;
then A16: D2 . j in A ;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A16, RCOMP_1:def 1;
then ex x being Real st
( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A8, A10;
then A17: D2 . j in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1;
( lower_bound (divset (D2,j)) = lower_bound A & upper_bound (divset (D2,j)) = D2 . j ) by A3, A13, INTEGRA1:def 4;
then divset (D2,j) = [.(lower_bound A),(D2 . j).] by INTEGRA1:4;
hence divset (D2,j) c= divset (D1,i) by A12, A15, A17, XXREAL_2:def 12; :: thesis: verum

end;

suppose A18: j <> 1 ; :: thesis: divset (D2,j) c= divset (D1,i)

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A19: A = { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def 1;
( D2 . j in rng D2 & rng D2 c= A ) by A3, FUNCT_1:def 3, INTEGRA1:def 2;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A19;
then ex x being Real st
( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ;
then D2 . j in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A8, A10;
then A20: D2 . j in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A21: A = { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by RCOMP_1:def 1;
A22: rng D2 c= A by INTEGRA1:def 2;
A23: j - 1 in dom D2 by A3, A18, INTEGRA1:7;
then D2 . (j - 1) in rng D2 by FUNCT_1:def 3;
then D2 . (j - 1) in { r where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A21, A22;
then A24: ex x being Real st
( x = D2 . (j - 1) & lower_bound A <= x & x <= upper_bound A ) ;
j <= j + 1 by NAT_1:11;
then j - 1 <= j by XREAL_1:20;
then D2 . (j - 1) <= D2 . j by A3, A23, SEQ_4:137;
then D2 . (j - 1) <= D1 . i by A8, A10, XXREAL_0:2;
then D2 . (j - 1) in { r where r is Real : ( lower_bound A <= r & r <= D1 . i ) } by A24;
then A25: D2 . (j - 1) in [.(lower_bound A),(D1 . i).] by RCOMP_1:def 1;
( lower_bound (divset (D2,j)) = D2 . (j - 1) & upper_bound (divset (D2,j)) = D2 . j ) by A3, A18, INTEGRA1:def 4;
then divset (D2,j) = [.(D2 . (j - 1)),(D2 . j).] by INTEGRA1:4;
hence divset (D2,j) c= divset (D1,i) by A12, A25, A20, XXREAL_2:def 12; :: thesis: verum

end;

end;

end;

hence divset (D2,j) c= divset (D1,i) ; :: thesis: verum

end;

suppose A26: i <> 1 ; :: thesis: divset (D2,j) c= divset (D1,i)

A27: j <> 1

proof

assume A28: j = 1 ; :: thesis: contradiction
A29: i in Seg (len D1) by A9, FINSEQ_1:def 3;
then A30: 1 <= i by FINSEQ_1:1;
i <= len D1 by A29, FINSEQ_1:1;
then 1 <= len D1 by A30, XXREAL_0:2;
then 1 in Seg (len D1) by FINSEQ_1:1;
then A31: 1 in dom D1 by FINSEQ_1:def 3;
then A32: D1 . 1 in rng D1 by FUNCT_1:def 3;
rng D1 c= rng D2 by A1, INTEGRA1:def 18;
then consider n being Element of NAT such that
A33: n in dom D2 and
A34: D1 . 1 = D2 . n by A32, PARTFUN1:3;
A35: n in Seg (len D2) by A33, FINSEQ_1:def 3;
then A36: 1 <= n by FINSEQ_1:1;
n <= len D2 by A35, FINSEQ_1:1;
then 1 <= len D2 by A36, XXREAL_0:2;
then 1 in Seg (len D2) by FINSEQ_1:1;
then 1 in dom D2 by FINSEQ_1:def 3;
then D2 . j <= D2 . n by A28, A33, A36, SEQ_4:137;
then n in X by A2, A32, A33, A34;
then n >= min X by XXREAL_2:def 7;
then A37: D1 . 1 >= D1 . i by A7, A10, A33, A34, SEQ_4:137;
i > 1 by A26, A30, XXREAL_0:1;
hence contradiction by A9, A31, A37, SEQM_3:def 1; :: thesis: verum

end;

then A38: j - 1 in dom D2 by A3, INTEGRA1:7;
A39: D1 . (i - 1) <= D2 . (j - 1)

proof

A40: i - 1 in dom D1 by A9, A26, INTEGRA1:7;
then A41: D1 . (i - 1) in rng D1 by FUNCT_1:def 3;
rng D1 c= rng D2 by A1, INTEGRA1:def 18;
then consider n being Element of NAT such that
A42: ( n in dom D2 & D1 . (i - 1) = D2 . n ) by A41, PARTFUN1:3;
assume D1 . (i - 1) > D2 . (j - 1) ; :: thesis: contradiction
then n > j - 1 by A38, A42, SEQ_4:137;
then n + 1 > j by XREAL_1:19;
then n >= j by NAT_1:13;
then D1 . (i - 1) >= D2 . j by A3, A42, SEQ_4:137;
then n in X by A2, A41, A42;
then n >= min X by XXREAL_2:def 7;
then D1 . (i - 1) >= D1 . i by A7, A10, A42, SEQ_4:137;
then i - 1 >= i by A9, A40, SEQM_3:def 1;
then A43: i >= i + 1 by XREAL_1:19;
i <= i + 1 by NAT_1:11;
then i = i + 1 by A43, XXREAL_0:1;
hence contradiction ; :: thesis: verum

end;

j <= j + 1 by NAT_1:11;
then j - 1 <= j by XREAL_1:20;
then A44: D2 . (j - 1) <= D2 . j by A3, A38, SEQ_4:137;
then A45: D1 . (i - 1) <= D2 . j by A39, XXREAL_0:2;
D2 . (j - 1) <= D1 . i by A11, A44, XXREAL_0:2;
then D2 . (j - 1) in { r where r is Real : ( D1 . (i - 1) <= r & r <= D1 . i ) } by A39;
then A46: D2 . (j - 1) in [.(D1 . (i - 1)),(D1 . i).] by RCOMP_1:def 1;
D2 . j <= D1 . i by A2, A7, A10;
then D2 . j in { r where r is Real : ( D1 . (i - 1) <= r & r <= D1 . i ) } by A45;
then A47: D2 . j in [.(D1 . (i - 1)),(D1 . i).] by RCOMP_1:def 1;
( lower_bound (divset (D2,j)) = D2 . (j - 1) & upper_bound (divset (D2,j)) = D2 . j ) by A3, A27, INTEGRA1:def 4;
then A48: divset (D2,j) = [.(D2 . (j - 1)),(D2 . j).] by INTEGRA1:4;
( lower_bound (divset (D1,i)) = D1 . (i - 1) & upper_bound (divset (D1,i)) = D1 . i ) by A9, A26, INTEGRA1:def 4;
then divset (D1,i) = [.(D1 . (i - 1)),(D1 . i).] by INTEGRA1:4;
hence divset (D2,j) c= divset (D1,i) by A48, A46, A47, XXREAL_2:def 12; :: thesis: verum

end;

end;

end;

hence divset (D2,j) c= divset (D1,i) ; :: thesis: verum

end;

hence ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) by A9; :: thesis: verum