let A be non empty closed_interval Subset of REAL; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: |.(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;

per cases ( s < t or not s < t ) ;

suppose s < t ; :: thesis: |.(s - t).| < r

then s - t < t - t by XREAL_1:14;
then |.(s - t).| = - (s - t) by ABSVALUE:def 1;
hence |.(s - t).| < r by A3, A4, XXREAL_0:2; :: thesis: verum

end;

suppose not s < t ; :: thesis: |.(s - t).| < r

then t - t <= s - t by XREAL_1:9;
then |.(s - t).| = s - t by ABSVALUE:def 1;
hence |.(s - t).| < r by A3, A4, XXREAL_0:2; :: thesis: verum

end;

end;