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 ;
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 ;
hence x in divset (D,j) by ; :: 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 ;
hence x in divset (D,j) by ; :: 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 S1[ 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 ; :: 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 ; :: thesis: verum
end;
end;
end;
then A14: upper_bound (divset (D,(len D))) = upper_bound A by INTEGRA1:def 2;
x <> upper_bound A then x < upper_bound (divset (D,(len D))) by ;
then A15: ex k being Nat st S1[k] by A13;
consider k being Nat such that
A16: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from defpred S2[ Nat] means ( x >= lower_bound (divset (D,\$1)) & \$1 in dom D );
lower_bound (divset (D,1)) = lower_bound A by ;
then A17: ex k being Nat st S2[k] by ;
A18: for k being Nat st S2[k] holds
k <= len D by FINSEQ_3:25;
consider j being Nat such that
A19: ( S2[j] & ( for n being Nat st S2[n] holds
n <= j ) ) from k = j
proof
assume A20: k <> j ; :: thesis: contradiction
per cases ( k < j or k > j ) by ;
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 ; :: thesis: verum
end;
suppose k <> 1 ; :: thesis: upper_bound (divset (D,k)) = D . k
hence upper_bound (divset (D,k)) = D . k by ; :: thesis: verum
end;
end;
end;
A23: 1 <= k by ;
then D . (j - 1) <= x by ;
then A24: D . (j - 1) < D . k by ;
j - 1 in dom D by ;
then j - 1 < k by ;
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 ; :: thesis: verum
end;
suppose j <> 1 ; :: thesis: upper_bound (divset (D,j)) = D . j
hence upper_bound (divset (D,j)) = D . j by ; :: thesis: verum
end;
end;
end;
assume A27: x >= upper_bound (divset (D,j)) ; :: thesis: contradiction
A28: j + 1 <= k by ;
A29: 1 <= j by ;
then A30: 1 <= j + 1 by NAT_1:13;
k <= len D by ;
then j + 1 <= len D by ;
then A31: j + 1 in dom D by ;
j + 1 > 1 by ;
then lower_bound (divset (D,(j + 1))) = D . ((j + 1) - 1) by
.= 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 ;
hence ex j being Element of NAT st
( j in dom D & x in divset (D,j) ) by A16; :: thesis: verum
end;
end;