let x be real number ; :: thesis: ( x >= 1 implies sqrt ((x + 1) / 2) >= 1 )
assume x >= 1 ; :: thesis: sqrt ((x + 1) / 2) >= 1
then x + 1 >= 1 + 1 by XREAL_1:8;
then (x + 1) / 2 >= 1 by XREAL_1:183;
hence sqrt ((x + 1) / 2) >= 1 by SQUARE_1:83, SQUARE_1:94; :: thesis: verum