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_{1}[ 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_{1}[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 )

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)

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

consider X being Subset of (dom D2) such that

A2: for x1 being set holds

( x1 in X iff ( x1 in dom D2 & S

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

then reconsider X = X as non empty Subset of NAT by A2;
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;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

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

end;

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

hence
divset (D2,j) c= divset (D1,i)
; :: thesis: verumper cases
( i = 1 or i <> 1 )
;

end;

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;

end;then A12: divset (D1,i) = [.(lower_bound A),(D1 . i).] by INTEGRA1:4;

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

hence
divset (D2,j) c= divset (D1,i)
; :: thesis: verumper cases
( j = 1 or j <> 1 )
;

end;

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;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

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;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

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

A27:
j <> 1

A39: D1 . (i - 1) <= D2 . (j - 1)

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;proof

then A38:
j - 1 in dom D2
by A3, INTEGRA1:7;
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;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

A39: D1 . (i - 1) <= D2 . (j - 1)

proof

j <= j + 1
by NAT_1:11;
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;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

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