let A be non empty closed_interval Subset of REAL; for D being Division of A
for r being Real st delta D < r holds
for i being Nat
for s, t being Real st i in dom D & s in divset (D,i) & t in divset (D,i) holds
|.(s - t).| < r
let D be Division of A; for r being Real st delta D < r holds
for i being Nat
for s, t being Real st i in dom D & s in divset (D,i) & t in divset (D,i) holds
|.(s - t).| < r
let r be Real; ( delta D < r implies for i being Nat
for s, t being Real st i in dom D & s in divset (D,i) & t in divset (D,i) holds
|.(s - t).| < r )
assume A1:
delta D < r
; for i being Nat
for s, t being Real st i in dom D & s in divset (D,i) & t in divset (D,i) holds
|.(s - t).| < r
let i be Nat; for s, t being Real st i in dom D & s in divset (D,i) & t in divset (D,i) holds
|.(s - t).| < r
let s, t be Real; ( i in dom D & s in divset (D,i) & t in divset (D,i) implies |.(s - t).| < r )
assume A2:
( i in dom D & s in divset (D,i) & t in divset (D,i) )
; |.(s - t).| < r
then
vol (divset (D,i)) <= delta D
by Th11;
then A3:
(upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) < r
by A1, XXREAL_0:2;
( s <= upper_bound (divset (D,i)) & t <= upper_bound (divset (D,i)) & lower_bound (divset (D,i)) <= s & lower_bound (divset (D,i)) <= t )
by A2, SEQ_4:def 1, SEQ_4:def 2;
then A4:
( t - s <= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) & s - t <= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) )
by XREAL_1:13;