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