let x be Real; :: 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:6;
then (x + 1) / 2 >= 1 by XREAL_1:181;
hence sqrt ((x + 1) / 2) >= 1 by SQUARE_1:18, SQUARE_1:26; :: thesis: verum