let a be positive Real; :: thesis: ( 1 / 2 < frac a implies frac (2 * a) < frac a )
assume A1: 1 / 2 < frac a ; :: thesis: frac (2 * a) < frac a
then reconsider a = a as non integer Real ;
A2: frac a < 1 by COMPLEX3:1;
then ( 2 * (1 / 2) < 2 * (frac a) & 2 * (frac a) < 2 * 1 ) by A1, XREAL_1:68;
then ( 1 - 1 < (2 * (frac a)) - 1 & (2 * (frac a)) - 1 < 2 - 1 ) by XREAL_1:9;
then reconsider y = (2 * (frac a)) - 1 as positive light Real by COMPLEX3:1;
(frac a) + (frac a) < (frac a) + 1 by XREAL_1:6, A2;
then A5: (2 * (frac a)) - 1 < ((frac a) + 1) - 1 by XREAL_1:9;
frac (y + 1) = y ;
hence frac (2 * a) < frac a by A5, FR3; :: thesis: verum