for x being Real st x >= 1 holds
sqrt ((x + 1) / 2) >= 1