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