let t be 1 _greater Nat; :: thesis: for r being Real st r in [.0,1.[ holds
ex i being Nat st
( i <= t - 1 & [\(r * t)/] = i )
let r be Real; :: thesis: ( r in [.0,1.[ implies ex i being Nat st
( i <= t - 1 & [\(r * t)/] = i ) )
assume r in [.0,1.[ ; :: thesis: ex i being Nat st
( i <= t - 1 & [\(r * t)/] = i )
then consider i being Nat such that
A2: i <= t - 1 and
A3: r in (Equal_Div_interval t) . i by Lm7;
thus ex i being Nat st
( i <= t - 1 & [\(r * t)/] = i ) by A2, Lm8, A3; :: thesis: verum