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