let i be Nat; :: thesis: for r1, r2 being Real
for t being 1 _greater Nat st r1 in (Equal_Div_interval t) . i & r2 in (Equal_Div_interval t) . i holds
|.(r1 - r2).| < t "
let r1, r2 be Real; :: thesis: for t being 1 _greater Nat st r1 in (Equal_Div_interval t) . i & r2 in (Equal_Div_interval t) . i holds
|.(r1 - r2).| < t "
let t be 1 _greater Nat; :: thesis: ( r1 in (Equal_Div_interval t) . i & r2 in (Equal_Div_interval t) . i implies |.(r1 - r2).| < t " )
assume that
A2: r1 in (Equal_Div_interval t) . i and
A3: r2 in (Equal_Div_interval t) . i ; :: thesis: |.(r1 - r2).| < t "
A5: ( r1 in [.(i / t),((i / t) + (t ")).[ & r1 in [.(i / t),((i / t) + (t ")).[ & r2 in [.(i / t),((i / t) + (t ")).[ ) by A2, A3, Def1;
then A6: ( i / t <= r1 & i / t <= r2 & r1 < (i / t) + (t ") & r2 < (i / t) + (t ") ) by XXREAL_1:3;

per cases ( r1 = r2 or r1 > r2 or r2 > r1 ) by XXREAL_0:1;

suppose r1 = r2 ; :: thesis: |.(r1 - r2).| < t "

then |.(r1 - r2).| = 0 by ABSVALUE:2;
hence |.(r1 - r2).| < t " by Lm1; :: thesis: verum

end;

suppose r1 > r2 ; :: thesis: |.(r1 - r2).| < t "

then A9: r1 - r2 > 0 by XREAL_1:50;
((i * (t ")) + (t ")) - (i * (t ")) > r1 - r2 by A6, XREAL_1:14;
hence |.(r1 - r2).| < t " by A9, ABSVALUE:def 1; :: thesis: verum

end;

suppose A10: r2 > r1 ; :: thesis: |.(r1 - r2).| < t "

r2 < (i * (t ")) + (t ") by A5, XXREAL_1:3;
then A12: ((i * (t ")) + (t ")) - r1 > r2 - r1 by XREAL_1:14;
i * (t ") <= r1 by A5, XXREAL_1:3;
then A13: ((i * (t ")) + (t ")) - (i * (t ")) >= ((i * (t ")) + (t ")) - r1 by XREAL_1:13;
|.(r1 - r2).| = - (r1 - r2) by A10, XREAL_1:49, ABSVALUE:def 1;
hence |.(r1 - r2).| < t " by A13, A12, XXREAL_0:2; :: thesis: verum

end;

end;