let a, b be Real; :: thesis: ( a - b > 1 implies ex t being Integer st
( a > t & t > b ) )
reconsider t = [\a/] as Integer ;
assume A1: a - b > 1 ; :: thesis: ex t being Integer st
( a > t & t > b )
then (a - b) + b > 1 + b by XREAL_1:6;
then A2: a > 1 + b ;
A3: t <= a by INT_1:def 6;

per cases ( t <> a or t = a ) ;

suppose t <> a ; :: thesis: ex t being Integer st
( a > t & t > b )

then S1: t < a by A3, XXREAL_0:1;
take t ; :: thesis: ( a > t & t > b )
S3: a - 1 < t by INT_1:def 6;
(a - b) + b > 1 + b by A1, XREAL_1:6;
then a - 1 > (1 + b) - 1 by XREAL_1:6;
then b < t by S3, XXREAL_0:2;
hence ( a > t & t > b ) by S1; :: thesis: verum

end;

suppose S0: t = a ; :: thesis: ex t being Integer st
( a > t & t > b )

take t - 1 ; :: thesis: ( a > t - 1 & t - 1 > b )
a - 1 < a - 0 by XREAL_1:15;
then S1: t - 1 < a by S0;
a - 1 > (1 + b) - 1 by A2, XREAL_1:8;
hence ( a > t - 1 & t - 1 > b ) by S1, S0; :: thesis: verum

end;

end;