let t be 1 _greater Nat; :: thesis: for r being Real
for i being Nat st [\(r * t)/] = i holds
r in (Equal_Div_interval t) . i
let r be Real; :: thesis: for i being Nat st [\(r * t)/] = i holds
r in (Equal_Div_interval t) . i
let i be Nat; :: thesis: ( [\(r * t)/] = i implies r in (Equal_Div_interval t) . i )
assume [\(r * t)/] = i ; :: thesis: r in (Equal_Div_interval t) . i
then A3: ( i <= r * t & (r * t) - 1 < i ) by INT_1:def 6;
then i / t <= (r * t) / t by XREAL_1:64;
then i * (t ") <= r * (t * (t ")) ;
then A6: i * (t ") <= r * 1 by Lm1;
A7: ((r * t) - 1) + 1 < i + 1 by A3, XREAL_1:8;
0 < t " by Lm1;
then (r * t) * (t ") < (i + 1) * (t ") by A7, XREAL_1:68;
then r * (t * (t ")) < (i + 1) * (t ") ;
then r * 1 < (i + 1) / t by Lm1;
then r in [.(i / t),((i / t) + (t ")).[ by A6, XXREAL_1:3;
hence r in (Equal_Div_interval t) . i by Def1; :: thesis: verum