let r, t be Real; :: thesis: ( t > 0 implies ex i being Integer st
( t * i <= r & r <= t * (i + 1) ) )
assume A0: t > 0 ; :: thesis: ex i being Integer st
( t * i <= r & r <= t * (i + 1) )
defpred S₁[ Integer] means t * $1 <= r;
g: ex i1 being Integer st S₁[i1]

proof

take i1 = [\(r / t)/]; :: thesis: S₁[i1]
i1 <= r / t by INT_1:def 6;
then i1 * t <= (r / t) * t by A0, XREAL_1:64;
then t * i1 <= r / (t / t) by XCMPLX_1:82;
hence t * i1 <= r by A0, XCMPLX_1:51; :: thesis: verum

end;

set F = [/(r / t)\];
f: for i1 being Integer st S₁[i1] holds
i1 <= [/(r / t)\]

proof

let i1 be Integer; :: thesis: ( S₁[i1] implies i1 <= [/(r / t)\] )
assume S₁[i1] ; :: thesis: i1 <= [/(r / t)\]
then (i1 * t) / t <= r / t by A0, XREAL_1:72;
then i1 * (t / t) <= r / t ;
then ( i1 * 1 <= r / t & r / t <= [/(r / t)\] ) by A0, XCMPLX_1:60, INT_1:def 7;
hence i1 <= [/(r / t)\] by XXREAL_0:2; :: thesis: verum

end;

consider i being Integer such that
i: ( S₁[i] & ( for i1 being Integer st S₁[i1] holds
i1 <= i ) ) from INT_1:sch 6(f, g);
take i ; :: thesis: ( t * i <= r & r <= t * (i + 1) )
thus t * i <= r by i; :: thesis: r <= t * (i + 1)
i + 1 > i + 0 by XREAL_1:6;
hence r <= t * (i + 1) by i; :: thesis: verum