theorem :: XREAL_1:220

for a being Real st a >= 1 / 2 holds
0 >= 1 - (2 * a)