let x be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for D being Division of A st x in A holds

ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st x in A holds

ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

let D be Division of A; :: thesis: ( x in A implies ex j being Element of NAT st

( j in dom D & x in divset (D,j) ) )

assume A1: x in A ; :: thesis: ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

then A2: lower_bound A <= x by INTEGRA2:1;

A3: x <= upper_bound A by A1, INTEGRA2:1;

A4: rng D <> {} ;

then A5: 1 in dom D by FINSEQ_3:32;

for D being Division of A st x in A holds

ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st x in A holds

ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

let D be Division of A; :: thesis: ( x in A implies ex j being Element of NAT st

( j in dom D & x in divset (D,j) ) )

assume A1: x in A ; :: thesis: ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

then A2: lower_bound A <= x by INTEGRA2:1;

A3: x <= upper_bound A by A1, INTEGRA2:1;

A4: rng D <> {} ;

then A5: 1 in dom D by FINSEQ_3:32;

per cases
( x in rng D or not x in rng D )
;

end;

suppose
x in rng D
; :: thesis: ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

( j in dom D & x in divset (D,j) )

then consider j being Element of NAT such that

A6: j in dom D and

A7: D . j = x by PARTFUN1:3;

x in divset (D,j)

( j in dom D & x in divset (D,j) ) by A6; :: thesis: verum

end;A6: j in dom D and

A7: D . j = x by PARTFUN1:3;

x in divset (D,j)

proof
end;

hence
ex j being Element of NAT st per cases
( j = 1 or j <> 1 )
;

end;

suppose A8:
j = 1
; :: thesis: x in divset (D,j)

A9:
ex a, b being Real st

( a <= b & a = lower_bound (divset (D,j)) & b = upper_bound (divset (D,j)) ) by SEQ_4:11;

upper_bound (divset (D,j)) = D . j by A6, A8, INTEGRA1:def 4;

hence x in divset (D,j) by A7, A9, INTEGRA2:1; :: thesis: verum

end;( a <= b & a = lower_bound (divset (D,j)) & b = upper_bound (divset (D,j)) ) by SEQ_4:11;

upper_bound (divset (D,j)) = D . j by A6, A8, INTEGRA1:def 4;

hence x in divset (D,j) by A7, A9, INTEGRA2:1; :: thesis: verum

suppose A10:
j <> 1
; :: thesis: x in divset (D,j)

A11:
ex a, b being Real st

( a <= b & a = lower_bound (divset (D,j)) & b = upper_bound (divset (D,j)) ) by SEQ_4:11;

upper_bound (divset (D,j)) = D . j by A6, A10, INTEGRA1:def 4;

hence x in divset (D,j) by A7, A11, INTEGRA2:1; :: thesis: verum

end;( a <= b & a = lower_bound (divset (D,j)) & b = upper_bound (divset (D,j)) ) by SEQ_4:11;

upper_bound (divset (D,j)) = D . j by A6, A10, INTEGRA1:def 4;

hence x in divset (D,j) by A7, A11, INTEGRA2:1; :: thesis: verum

( j in dom D & x in divset (D,j) ) by A6; :: thesis: verum

suppose A12:
not x in rng D
; :: thesis: ex j being Element of NAT st

( j in dom D & x in divset (D,j) )

( j in dom D & x in divset (D,j) )

defpred S_{1}[ Nat] means ( x < upper_bound (divset (D,$1)) & $1 in dom D );

A13: len D in dom D by FINSEQ_5:6;

upper_bound (divset (D,(len D))) = D . (len D)

x <> upper_bound A

then A15: ex k being Nat st S_{1}[k]
by A13;

consider k being Nat such that

A16: ( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A15);

defpred S_{2}[ Nat] means ( x >= lower_bound (divset (D,$1)) & $1 in dom D );

lower_bound (divset (D,1)) = lower_bound A by A5, INTEGRA1:def 4;

then A17: ex k being Nat st S_{2}[k]
by A2, A4, FINSEQ_3:32;

A18: for k being Nat st S_{2}[k] holds

k <= len D by FINSEQ_3:25;

consider j being Nat such that

A19: ( S_{2}[j] & ( for n being Nat st S_{2}[n] holds

n <= j ) ) from NAT_1:sch 6(A18, A17);

k = j

hence ex j being Element of NAT st

( j in dom D & x in divset (D,j) ) by A16; :: thesis: verum

end;A13: len D in dom D by FINSEQ_5:6;

upper_bound (divset (D,(len D))) = D . (len D)

proof
end;

then A14:
upper_bound (divset (D,(len D))) = upper_bound A
by INTEGRA1:def 2;x <> upper_bound A

proof

then
x < upper_bound (divset (D,(len D)))
by A3, A14, XXREAL_0:1;
assume
x = upper_bound A
; :: thesis: contradiction

then x = D . (len D) by INTEGRA1:def 2;

hence contradiction by A12, A13, FUNCT_1:def 3; :: thesis: verum

end;then x = D . (len D) by INTEGRA1:def 2;

hence contradiction by A12, A13, FUNCT_1:def 3; :: thesis: verum

then A15: ex k being Nat st S

consider k being Nat such that

A16: ( S

k <= n ) ) from NAT_1:sch 5(A15);

defpred S

lower_bound (divset (D,1)) = lower_bound A by A5, INTEGRA1:def 4;

then A17: ex k being Nat st S

A18: for k being Nat st S

k <= len D by FINSEQ_3:25;

consider j being Nat such that

A19: ( S

n <= j ) ) from NAT_1:sch 6(A18, A17);

k = j

proof

then
x in divset (D,k)
by A16, A19, INTEGRA2:1;
assume A20:
k <> j
; :: thesis: contradiction

end;per cases
( k < j or k > j )
by A20, XXREAL_0:1;

end;

suppose A21:
k < j
; :: thesis: contradiction

A22:
upper_bound (divset (D,k)) = D . k

then D . (j - 1) <= x by A19, A21, INTEGRA1:def 4;

then A24: D . (j - 1) < D . k by A16, A22, XXREAL_0:2;

j - 1 in dom D by A19, A21, A23, INTEGRA1:7;

then j - 1 < k by A16, A24, SEQ_4:137;

then j < k + 1 by XREAL_1:19;

hence contradiction by A21, NAT_1:13; :: thesis: verum

end;proof
end;

A23:
1 <= k
by A16, FINSEQ_3:25;then D . (j - 1) <= x by A19, A21, INTEGRA1:def 4;

then A24: D . (j - 1) < D . k by A16, A22, XXREAL_0:2;

j - 1 in dom D by A19, A21, A23, INTEGRA1:7;

then j - 1 < k by A16, A24, SEQ_4:137;

then j < k + 1 by XREAL_1:19;

hence contradiction by A21, NAT_1:13; :: thesis: verum

suppose A25:
k > j
; :: thesis: contradiction

x < upper_bound (divset (D,j))

end;proof

hence
contradiction
by A16, A19, A25; :: thesis: verum
A26:
upper_bound (divset (D,j)) = D . j

A28: j + 1 <= k by A25, NAT_1:13;

A29: 1 <= j by A19, FINSEQ_3:25;

then A30: 1 <= j + 1 by NAT_1:13;

k <= len D by A16, FINSEQ_3:25;

then j + 1 <= len D by A28, XXREAL_0:2;

then A31: j + 1 in dom D by A30, FINSEQ_3:25;

j + 1 > 1 by A29, NAT_1:13;

then lower_bound (divset (D,(j + 1))) = D . ((j + 1) - 1) by A31, INTEGRA1:def 4

.= D . j ;

then j + 1 <= j by A19, A27, A26, A31;

hence contradiction by NAT_1:13; :: thesis: verum

end;proof
end;

assume A27:
x >= upper_bound (divset (D,j))
; :: thesis: contradictionA28: j + 1 <= k by A25, NAT_1:13;

A29: 1 <= j by A19, FINSEQ_3:25;

then A30: 1 <= j + 1 by NAT_1:13;

k <= len D by A16, FINSEQ_3:25;

then j + 1 <= len D by A28, XXREAL_0:2;

then A31: j + 1 in dom D by A30, FINSEQ_3:25;

j + 1 > 1 by A29, NAT_1:13;

then lower_bound (divset (D,(j + 1))) = D . ((j + 1) - 1) by A31, INTEGRA1:def 4

.= D . j ;

then j + 1 <= j by A19, A27, A26, A31;

hence contradiction by NAT_1:13; :: thesis: verum

hence ex j being Element of NAT st

( j in dom D & x in divset (D,j) ) by A16; :: thesis: verum