let a be Real; :: thesis: ( 0 < a implies a / 3 < a )
assume A1: 0 < a ; :: thesis: a / 3 < a
then A2: ((a / 3) + (a / 3)) + 0 < ((a / 3) + (a / 3)) + (a / 3) by Lm10;
0 + (a / 3) < (a / 3) + (a / 3) by A1, Lm10;
hence a / 3 < a by A2, XXREAL_0:2; :: thesis: verum