theorem :: XREAL_1:219

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