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;

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

suppose x in rng D ; :: thesis: ex j being Element of NAT st
( 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)

proof

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

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;

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;

end;

end;

hence ex j being Element of NAT st
( j in dom D & x in divset (D,j) ) by A6; :: thesis: verum

end;

suppose A12: not x in rng D ; :: thesis: ex j being Element of NAT st
( j in dom D & x in divset (D,j) )

defpred S₁[ 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)

proof

per cases ( len D = 1 or len D <> 1 ) ;

suppose len D = 1 ; :: thesis: upper_bound (divset (D,(len D))) = D . (len D)

hence upper_bound (divset (D,(len D))) = D . (len D) by A13, INTEGRA1:def 4; :: thesis: verum

end;

suppose len D <> 1 ; :: thesis: upper_bound (divset (D,(len D))) = D . (len D)

hence upper_bound (divset (D,(len D))) = D . (len D) by A13, INTEGRA1:def 4; :: thesis: verum

end;

end;

end;

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

proof

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 < upper_bound (divset (D,(len D))) by A3, A14, XXREAL_0:1;
then A15: ex k being Nat st S₁[k] by A13;
consider k being Nat such that
A16: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A15);
defpred S₂[ 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₂[k] by A2, A4, FINSEQ_3:32;
A18: for k being Nat st S₂[k] holds
k <= len D by FINSEQ_3:25;
consider j being Nat such that
A19: ( S₂[j] & ( for n being Nat st S₂[n] holds
n <= j ) ) from NAT_1:sch 6(A18, A17);
k = j

proof

assume A20: k <> j ; :: thesis: contradiction

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

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

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

proof

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

suppose k = 1 ; :: thesis: upper_bound (divset (D,k)) = D . k

hence upper_bound (divset (D,k)) = D . k by A16, INTEGRA1:def 4; :: thesis: verum

end;

suppose k <> 1 ; :: thesis: upper_bound (divset (D,k)) = D . k

hence upper_bound (divset (D,k)) = D . k by A16, INTEGRA1:def 4; :: thesis: verum

end;

end;

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

end;

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

x < upper_bound (divset (D,j))

proof

A26: upper_bound (divset (D,j)) = D . j

proof

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

suppose j = 1 ; :: thesis: upper_bound (divset (D,j)) = D . j

hence upper_bound (divset (D,j)) = D . j by A19, INTEGRA1:def 4; :: thesis: verum

end;

suppose j <> 1 ; :: thesis: upper_bound (divset (D,j)) = D . j

hence upper_bound (divset (D,j)) = D . j by A19, INTEGRA1:def 4; :: thesis: verum

end;

end;

end;

assume A27: x >= upper_bound (divset (D,j)) ; :: thesis: contradiction
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;

hence contradiction by A16, A19, A25; :: thesis: verum

end;

end;

end;

then x in divset (D,k) by A16, A19, INTEGRA2:1;
hence ex j being Element of NAT st
( j in dom D & x in divset (D,j) ) by A16; :: thesis: verum

end;

end;