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 Lm16; :: thesis: verum