let a be Real; :: thesis: ( a <= 1 / 2 implies (2 * a) - 1 <= 0 )
assume a <= 1 / 2 ; :: thesis: (2 * a) - 1 <= 0
then 2 * a <= 2 * (1 / 2) by Lm12;
then 2 * a <= 1 + 0 ;
hence (2 * a) - 1 <= 0 by Lm18; :: thesis: verum