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